English
The canonical associator respects left injections: (sumAssoc I I M n M' M'') ∘ Sum.inl = Sum.inl ∘ Equiv.sumAssoc M M' M''.
Русский
Канонический ассоциатор сохраняет действие левой инъекции: ...
LaTeX
$$$ (sumAssoc I I M n M' M'') \\circ Sum.inl = Sum.inl \\circ Equiv.sumAssoc M M' M'' $$$
Lean4
/-- The canonical diffeomorphism `(M ⊕ N) ⊕ P → M ⊕ (N ⊕ P)` -/
def sumAssoc : Diffeomorph I I ((M ⊕ M') ⊕ M'') (M ⊕ (M' ⊕ M'')) n
where
toEquiv := Equiv.sumAssoc M M' M''
contMDiff_toFun := by
apply ContMDiff.sumElim
· exact contMDiff_id.sumMap ContMDiff.inl
· exact ContMDiff.inr.comp ContMDiff.inr
contMDiff_invFun := by
apply ContMDiff.sumElim
· exact ContMDiff.inl.comp ContMDiff.inl
· exact ContMDiff.inr.sumMap contMDiff_id
