The composition of kernels associates to the left: ξ ∘ₖ η ∘ₖ κ stands for (ξ ∘ₖ η) ∘ₖ κ. An equality h : η ∘ₖ κ = ζ therefore cannot rewrite this kernel, since η ∘ₖ κ is not one of its subterms: rw [h] fails, and one first has to reassociate with Kernel.comp_assoc. The composition ≫ of morphisms in a category raises the same issue, which Mathlib solves with the attribute @[reassoc]. From a lemma F : f = g with f g : X ⟶ Y, it generates the lemma F_assoc : ∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h, whose two sides are normalized with the associativity of ≫, so that F_assoc rewrites f inside longer compositions. The translation of kernels to morphisms of SFinKer allows to adapt this attribute to kernels.
@[kernel_reassoc] attribute
From a lemma F whose conclusion is f = g with f g : Kernel X Y s-finite kernels, @[kernel_reassoc] generates a lemma F_assoc with the same hypotheses and the conclusion
∀ {Z : Type u} [MeasurableSpace Z] (ξ : Kernel Y Z) [IsSFiniteKernel ξ], ξ ∘ₖ f = ξ ∘ₖ g,
where both sides are normalized so that all the compositions associate to the left. For instance:
@[kernel_reassoc]
lemma parallelComp_comp_prod₀ : (η ∥ₖ η') ∘ₖ (κ ×ₖ κ') = (η ∘ₖ κ) ×ₖ (η' ∘ₖ κ') := X:Type u_1Y:Type u_2Z:Type u_3Y':Type u_4Z':Type u_5inst✝⁸:MeasurableSpace Xinst✝⁷:MeasurableSpace Yinst✝⁶:MeasurableSpace Zinst✝⁵:MeasurableSpace Y'inst✝⁴:MeasurableSpace Z'κ:Kernel X Yinst✝³:IsSFiniteKernel κη:Kernel Y Zinst✝²:IsSFiniteKernel ηκ':Kernel X Y'inst✝¹:IsSFiniteKernel κ'η':Kernel Y' Z'inst✝:IsSFiniteKernel η'⊢ η ∥ₖ η' ∘ₖ (κ ×ₖ κ') = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
All goals completed! 🐙
#check parallelComp_comp_prod₀_assoc κ η κ' η' ξ
The products are written with ×ₖ in F_assoc, as in F, so that F_assoc rewrites the goals stated with them. The translation unfolds the products ×ₖ and composition-products ⊗ₖ, and the reassociation splits their unfoldings, but the translation back folds them, as described in the page on hom_kernel.
The attribute works by transport. The kernel equality is translated into an equality of morphisms of SFinKer, as in kernel_hom. The @[reassoc] pipeline of Mathlib is applied to this equality, and the result is translated back into kernels, as in hom_kernel. The only subtlety concerns universes. The translation lifts all the carriers of F to a common level w, so the lemma produced by @[reassoc] quantifies over the objects Z of SFinKer.{w} only. Translated back, it would not apply to a kernel ξ whose codomain lives in an arbitrary universe. The equality is therefore lifted to max u w, where u is a fresh level for Z, and u becomes a new universe parameter of F_assoc.
Core handler for @[kernel_reassoc].
Given an equality between s-finite kernels, this constructs the corresponding reassociated
equality in SFinKer category, under the extra Z measurable space and instance binders needed to
state the result. The returned array contains the fresh level metavariables that still need to be
added to the declaration's universe levels.
kernel_reassoc_of% elaborator
As @[reassoc] comes with the term elaborator reassoc_of%, @[kernel_reassoc] comes with kernel_reassoc_of%. For a proof h of an equality of s-finite kernels, kernel_reassoc_of% h is a proof of the reassociated equality, built as above. Unlike the attribute, it also applies to local hypotheses. For instance, it solves the rewriting problem described at the beginning of this page:
example {κ : Kernel X Y} {η : Kernel Y Z} {ζ : Kernel X Z} {ξ : Kernel Z W}
[IsSFiniteKernel κ] [IsSFiniteKernel η] [IsSFiniteKernel ζ] [IsSFiniteKernel ξ]
(h : η ∘ₖ κ = ζ) :
ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ ζ := X:Type u_1Y:Type u_2Z:Type u_3Y':Type u_4Z':Type u_5inst✝¹⁴:MeasurableSpace Xinst✝¹³:MeasurableSpace Yinst✝¹²:MeasurableSpace Zinst✝¹¹:MeasurableSpace Y'inst✝¹⁰:MeasurableSpace Z'κ✝:Kernel X Yinst✝⁹:IsSFiniteKernel κ✝η✝:Kernel Y Zinst✝⁸:IsSFiniteKernel η✝κ':Kernel X Y'inst✝⁷:IsSFiniteKernel κ'η':Kernel Y' Z'inst✝⁶:IsSFiniteKernel η'W:Type u_6inst✝⁵:MeasurableSpace Wξ✝:Kernel (Z × Z') Winst✝⁴:IsSFiniteKernel ξ✝κ:Kernel X Yη:Kernel Y Zζ:Kernel X Zξ:Kernel Z Winst✝³:IsSFiniteKernel κinst✝²:IsSFiniteKernel ηinst✝¹:IsSFiniteKernel ζinst✝:IsSFiniteKernel ξh:η ∘ₖ κ = ζ⊢ ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ ζ
All goals completed! 🐙