hom_kernel tactic

This file implements the hom_kernel tactic, the inverse of kernel_hom. It transforms equalities written in the monoidal category back into equivalent equalities of kernels.

Main declarations

• transformHomToKernel: recursive translation from categorical morphism expressions to kernel expressions.
• mkHomKernelEqProof: construction of the equivalence proof used by the tactic.
• applyHomKernel: core implementation on goals and hypotheses.
• hom_kernel: user-facing tactic (with location support).

partial def get_type_from_SFinKer (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Level)

Get the original type and its universe from a SFinKer.of expression.

def deconstruct_unitors_hom (iso : Lean.Expr) (eLevel : Lean.Level) (left : Bool) : Lean.MetaM (Lean.Expr × CategoryOP)

Deconstruct a left or right unitor morphism to get the underlying kernel

Equations

• One or more equations did not get rendered due to their size.

def deconstruct_unitors_inv (iso : Lean.Expr) (eLevel : Lean.Level) (left : Bool) : Lean.MetaM (Lean.Expr × CategoryOP)

Deconstruct a left or right unitor inverse morphism to get the underlying kernel

Equations

• One or more equations did not get rendered due to their size.

def deconstruct_whiskers_hom_args (e : Lean.Expr) (eLevel : Lean.Level) (left : Bool) : Lean.MetaM (Lean.Expr × Lean.Expr × CategoryOP)

Deconstruct a left or right whisker to get the underlying kernel and the whiskered object

Equations

• One or more equations did not get rendered due to their size.

def deconstruct_associator_hom (iso : Lean.Expr) (eLevel : Lean.Level) : Lean.MetaM (Lean.Expr × CategoryOP)

Deconstruct the associator morphism to get the underlying kernel

Equations

• One or more equations did not get rendered due to their size.

def deconstruct_associator_inv (iso : Lean.Expr) (eLevel : Lean.Level) : Lean.MetaM (Lean.Expr × CategoryOP)

Deconstruct the associator inverse morphism to get the underlying kernel

Equations

• One or more equations did not get rendered due to their size.

def deconstruct_braiding (iso : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

Deconstruct the braiding morphism to get the underlying swapped objects

Equations

• One or more equations did not get rendered due to their size.

partial def transformHomToKernel (eLevel : Lean.Level) (e : Lean.Expr) (op_data : List CategoryOP) : Lean.MetaM (Lean.Expr × List CategoryOP)

Recursive transformation from morphism expression in SFinKer to kernel expression.

def mkHomKernelEqProof (eqProofType : Lean.Expr) (eLevel : Lean.Level) (op_data : List CategoryOP) : Lean.Elab.Tactic.TacticM Lean.Expr

Construct the proof of equivalence between the original equality and the transformed one.

Equations

• One or more equations did not get rendered due to their size.

def ApplyHomKernel (goal : Lean.MVarId) (fvarId : Option Lean.FVarId) : Lean.Elab.Tactic.TacticM Lean.MVarId

The hom_kernel tactic is the inverse of kernel_hom: it transforms an equality written in the monoidal category back to an equivalent equality of s-finite kernels.

The tactic supports location specifiers like rw or simp:

• hom_kernel — applies to the goal
• hom_kernel at h — applies to hypothesis h
• hom_kernel at h₁ h₂ — applies to multiple hypotheses
• hom_kernel at h ⊢ — applies to hypothesis h and the goal
• hom_kernel at * — applies to all hypotheses and the goal

It is useful to switch back to kernel equations once categorical rewrites are done.

Equations

• One or more equations did not get rendered due to their size.

def homKernel : Lean.ParserDescr

The hom_kernel tactic is the inverse of kernel_hom: it transforms an equality written in the monoidal category back to an equivalent equality of s-finite kernels.

The tactic supports location specifiers like rw or simp:

• hom_kernel — applies to the goal
• hom_kernel at h — applies to hypothesis h
• hom_kernel at h₁ h₂ — applies to multiple hypotheses
• hom_kernel at h ⊢ — applies to hypothesis h and the goal
• hom_kernel at * — applies to all hypotheses and the goal

It is useful to switch back to kernel equations once categorical rewrites are done.

Equations

• One or more equations did not get rendered due to their size.