Categorical Kernel Reasoning

2. KernelHom tactic🔗

The kernel_hom tactic transforms a kernel equality into an equality in the SFinKer category, where categorical tactics can be applied to simplify it. For example, given kernels κ : Kernel X Y, η : Kernel Y Z and ξ : Kernel X Z, the following kernel equality: η ∘ₖ κ = ξ is transformed to κ.hom ≫ η.hom = ξ.hom in the SFinKer category, where hom is the translation of kernels to morphisms in SFinKer.

The tactic can be described in 4 steps:

  1. First, it finds the minimum common universe level for which all carrier spaces of the kernels involved in the equality can be lifted to.

  2. Then, it recursively traverses the kernel equality and creates a new expression where each kernel is replaced by its translation in the SFinKer category, uniformly lifting carrier spaces to the common universe level determined in the first step. During this process, it recognizes patterns of kernel composition and identities, and translates them to the corresponding categorical operations (composition, identity, unitors, whiskers, monoidal composition, etc...). This is done using the transformKernelToHom function.

  3. Next, it constructs the proof of equivalence between the original kernel equality and the transformed categorical equality. This proof relies on the properties of the translation (e.g., that it preserves composition and identities) and on the fact that all kernels can be uniformly lifted to the common universe level using measurable equivalences.

  4. Finally, it replaces the original goal or hypothesis with the transformed one.

2.1. Usage examples🔗

The tactic kernel_hom allows users to leverage categorical reasoning or powerful categorical tactics to simplify kernel equalities.

example : ξ ∘ₖ (η ∘ₖ κ) = ξ ∘ₖ η ∘ₖ κ := W:Type u_1X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:MeasurableSpace Winst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:MeasurableSpace Zκ:Kernel X Yη:Kernel Y Zξ:Kernel Z Winst✝²:IsFiniteKernel ξinst✝¹:IsSFiniteKernel κinst✝:IsSFiniteKernel η⊢ ξ ∘ₖ (η ∘ₖ κ) = ξ ∘ₖ η ∘ₖ κ W:Type u_1X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:MeasurableSpace Winst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:MeasurableSpace Zκ:Kernel X Yη:Kernel Y Zξ:Kernel Z Winst✝²:IsFiniteKernel ξinst✝¹:IsSFiniteKernel κinst✝:IsSFiniteKernel η⊢ (κ.hom ≫ η.hom) ≫ ξ.hom = κ.hom ≫ η.hom ≫ ξ.hom All goals completed! 🐙example : (η ∘ₖ Kernel.id.map (Prod.fst : Y × PUnit → Y)) ∘ₖ (Kernel.id.map (Prod.fst : Y × PUnit → Y) ∥ₖ Kernel.id (α := PUnit)) ∘ₖ ((κ ∥ₖ Kernel.id (α := PUnit)) ∥ₖ Kernel.id (α := PUnit)) = (η ∘ₖ κ ∘ₖ (Kernel.id.map (Prod.fst : X × PUnit → X)) ∘ₖ ((Kernel.id.map (Prod.fst : X × PUnit → X)) ∥ₖ Kernel.id (α := PUnit)) : Kernel ((X × PUnit) × PUnit) Z) := W:Type u_1X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:MeasurableSpace Winst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:MeasurableSpace Zκ:Kernel X Yη:Kernel Y Zξ:Kernel Z Winst✝²:IsFiniteKernel ξinst✝¹:IsSFiniteKernel κinst✝:IsSFiniteKernel η⊢ η ∘ₖ Kernel.id.map Prod.fst ∘ₖ (Kernel.id.map Prod.fst ∥ₖ Kernel.id) ∘ₖ (κ ∥ₖ Kernel.id ∥ₖ Kernel.id) = η ∘ₖ κ ∘ₖ Kernel.id.map Prod.fst ∘ₖ (Kernel.id.map Prod.fst ∥ₖ Kernel.id) W:Type u_1X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:MeasurableSpace Winst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:MeasurableSpace Zκ:Kernel X Yη:Kernel Y Zξ:Kernel Z Winst✝²:IsFiniteKernel ξinst✝¹:IsSFiniteKernel κinst✝:IsSFiniteKernel η⊢ κ.hom ▷ 𝟙_ SFinKer ▷ 𝟙_ SFinKer ≫ (ρ_ { carrier := ULift.{max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (u_2 + 1) (u_4 + 1)) (u_5 + 1)) (u_6 + 1)) u_6 u_5 u_2) u_4) u_5 u_2) u_6) u_2) u_5) (u_5 + 1)) (u_6 + 1)) u_6 u_3 u_5) u_3 u_5) u_3) u_3 u_6) (max u_2 u_6) u_5) u_2 u_6) u_2 u_5, u_3} Y, str := ULift.instMeasurableSpace }).hom ▷ 𝟙_ SFinKer ≫ (ρ_ { carrier := ULift.{max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (u_2 + 1) (u_4 + 1)) (u_5 + 1)) (u_6 + 1)) u_6 u_5 u_2) u_4) u_5 u_2) u_6) u_2) u_5) (u_5 + 1)) (u_6 + 1)) u_6 u_3 u_5) u_3 u_5) u_3) u_3 u_6) (max u_2 u_6) u_5) u_2 u_6) u_2 u_5, u_3} Y, str := ULift.instMeasurableSpace }).hom ≫ η.hom = (ρ_ { carrier := ULift.{max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (u_2 + 1) (u_4 + 1)) (u_5 + 1)) (u_6 + 1)) u_6 u_5 u_2) u_4) u_5 u_2) u_6) u_2) u_5) (u_5 + 1)) (u_6 + 1)) u_6 u_3 u_5) u_3 u_5) u_3) u_3 u_6) (max u_2 u_6) u_5) u_2 u_6) u_2 u_5, u_2} X, str := ULift.instMeasurableSpace }).hom ▷ 𝟙_ SFinKer ≫ (ρ_ { carrier := ULift.{max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (max (u_2 + 1) (u_4 + 1)) (u_5 + 1)) (u_6 + 1)) u_6 u_5 u_2) u_4) u_5 u_2) u_6) u_2) u_5) (u_5 + 1)) (u_6 + 1)) u_6 u_3 u_5) u_3 u_5) u_3) u_3 u_6) (max u_2 u_6) u_5) u_2 u_6) u_2 u_5, u_2} X, str := ULift.instMeasurableSpace }).hom ≫ κ.hom ≫ η.hom; All goals completed! 🐙