toLaxMonoidal_injective — Mathlib

English

There is a natural isomorphism μNatIso between the tensoring of F with itself and the tensoring after F, i.e., a canonical tensorator for F.

Русский

Существует естественная изоморфность μNatIso между F×F ⋙ tensor_D и tensor_C ⋙ F.

LaTeX

$$$$ \\mu\\mathrm{NatIso} : (F \\mathrm{prod} F) \\;\\circ\\; \\mathrm{tensor}_D \\cong \\mathrm{tensor}_C \\circ F $$$$

Lean4

theorem toLaxMonoidal_injective :
    Function.Injective (@Monoidal.toLaxMonoidal _ _ _ _ _ _ _ : F.Monoidal → F.LaxMonoidal) :=
  by
  intro a b eq
  ext1
  · exact congr(($eq).ε)
  · exact congr(($eq).μ)
  · rw [← cancel_epi (εIso _).hom]
    rw [εIso_hom, ε_η, ← @ε_η _ _ _ _ _ _ _ a, ← εIso_hom]
    exact congr(($eq.symm).ε ≫ _)
  · ext
    rw [← cancel_epi (μIso F _ _).hom]
    rw [μIso_hom, μ_δ, ← @μ_δ _ _ _ _ _ _ _ a, ← μIso_hom]
    exact congr(($eq.symm).μ _ _ ≫ _)

Похожие утверждения