homEquiv_naturality_str_symm — Mathlib

English

Symmetric naturlaity of the hom-equivalence in adjunctions on coalgebras.

Русский

Симметричная естественность гомоэквивалентности в сопряжениях над коалгебрами.

LaTeX

$$$\forall\, adj:\ F \dashv G,\ V_1,V_2:\ Coalgebra\ G,\ f:\ V_1 \to V_2,\ F.map f.f \; \circ \; (adj.homEquiv V_2.V V_2.V).symm V_2.str = (adj.homEquiv V_1.V V_1.V).symm V_1.str \; \circ \; f.f$$$

Lean4

theorem homEquiv_naturality_str_symm (adj : F ⊣ G) (V₁ V₂ : Coalgebra G) (f : V₁ ⟶ V₂) :
    F.map f.f ≫ (adj.homEquiv V₂.V V₂.V).symm V₂.str = (adj.homEquiv V₁.V V₁.V).symm V₁.str ≫ f.f := by
  rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm, f.h]

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