kernel_hom tactic

This file implements the kernel_hom tactic, which transforms equalities of kernels into equivalent equalities in the monoidal category.

Main declarations

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

def check_unitors (κ : Lean.Expr) (offset : ℕ) (prod : Lean.Name) : Lean.MetaM Bool

Check if a kernel expression corresponds to a left or right unitor.

Equations

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

def check_leftUnitor (κ : Lean.Expr) : Lean.MetaM Bool

Check if a kernel expression corresponds to a left unitor.

Equations

• check_leftUnitor κ = check_unitors κ 0 `Prod.snd

def check_rightUnitor (κ : Lean.Expr) : Lean.MetaM Bool

Check if a kernel expression corresponds to a right unitor.

Equations

• check_rightUnitor κ = check_unitors κ 1 `Prod.fst

partial def decomposeProductToSFinker (X : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM Lean.Expr

Recursively decompose a product type into SFinKer objects with monoidal tensor structure.

def compute_SFinkerOf (X : Lean.Expr) (xLvl maxLvl : Lean.Level) : Lean.MetaM Lean.Expr

Compute the SFinKer object corresponding to a measurable space.

Equations

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

def construct_unitors (X Y : Lean.Expr) (yLvl maxLvl : Lean.Level) (offset : ℕ) : Lean.MetaM (Lean.Expr × CategoryOP)

Construct the left or right unitor morphism.

Equations

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

def check_Whiskers (κ : Lean.Expr) (offset : ℕ) : Lean.MetaM Bool

Check if a kernel expression corresponds to a left or right whisker.

Equations

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

def check_WhiskerLeft (κ : Lean.Expr) : Lean.MetaM Bool

Check if a kernel expression corresponds to a left whisker.

Equations

• check_WhiskerLeft κ = check_Whiskers κ 2

def check_WhiskerRight (κ : Lean.Expr) : Lean.MetaM Bool

Check if a kernel expression corresponds to a right whisker.

Equations

• check_WhiskerRight κ = check_Whiskers κ 1

def construct_whiskers_args (e X : Lean.Expr) (maxLvl : Lean.Level) (offset : ℕ) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Level)

Construct the relevant data for converting a kernel expression to its whisker morphism representation.

Equations

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

def check_associator (κ : Lean.Expr) (hom : Bool) : Lean.MetaM Bool

Check if a kernel expression corresponds to an associator morphism or its inverse.

Equations

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

def check_associator_hom (κ : Lean.Expr) : Lean.MetaM Bool

Check if a kernel expression corresponds to an associator morphism.

Equations

• check_associator_hom κ = check_associator κ true

def check_associator_inv (κ : Lean.Expr) : Lean.MetaM Bool

Check if a kernel expression corresponds to an inverse associator morphism.

Equations

• check_associator_inv κ = check_associator κ false

def get_types_from_three_prods (prod : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Level × Lean.Level × Lean.Level)

Get the types and universe levels from a expression of the form X × Y × Z.

Equations

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

def construct_associator (left right : Lean.Expr) (maxLvl : Lean.Level) (hom : Bool) : Lean.MetaM (Lean.Expr × CategoryOP)

Construct the associator morphism or its inverse.

Equations

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

def construct_associator_hom (left right : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × CategoryOP)

Construct the associator morphism.

Equations

• construct_associator_hom left right maxLvl = construct_associator left right maxLvl true

def construct_associator_inv (left right : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × CategoryOP)

Construct the inverse associator morphism.

Equations

• construct_associator_inv left right maxLvl = construct_associator left right maxLvl false

partial def transformKernelToHom (maxLvl : Lean.Level) (e : Lean.Expr) (op_data : List CategoryOP) : Lean.MetaM (Lean.Expr × List CategoryOP)

Recursive transformation from kernel expressions to morphism expressions in the SFinKer category.

def mkKernelHomEqProof (eqProofType rhs lhs : Lean.Expr) (maxLvl : 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 ApplyKernelHom (goal : Lean.MVarId) (fvarId : Option Lean.FVarId) : Lean.Elab.Tactic.TacticM Lean.MVarId

The kernel_hom tactic transforms a kernel equality to an equivalent equality in the category of measurable spaces and s-finite kernels.

The tactic supports location specifiers like rw or simp:

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

Example:

example {W X Y Z : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z]
    [MeasurableSpace W] (κ : Kernel X Y) (η : Kernel Y Z) (ξ : Kernel Z W)
    [IsFiniteKernel ξ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    ξ ∘ₖ (η ∘ₖ κ) = ξ ∘ₖ η ∘ₖ κ := by
  kernel_hom
  exact Category.assoc _ _ _

Equations

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

def kernelHom : Lean.ParserDescr

The kernel_hom tactic transforms a kernel equality to an equivalent equality in the category of measurable spaces and s-finite kernels.

The tactic supports location specifiers like rw or simp:

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

Example:

example {W X Y Z : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z]
    [MeasurableSpace W] (κ : Kernel X Y) (η : Kernel Y Z) (ξ : Kernel Z W)
    [IsFiniteKernel ξ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    ξ ∘ₖ (η ∘ₖ κ) = ξ ∘ₖ η ∘ₖ κ := by
  kernel_hom
  exact Category.assoc _ _ _

Equations

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