homEquiv_naturality_str — Mathlib

English

Naturality of the hom-equivalence in an adjunction between F and G on algebras: the hom-equivalence commutes with structure maps.

Русский

Естественность гомоэквивалентности в паре перестановок F ⊣ G на алгебрах: гомоэквивалентность взаимодействует со структурами алгебр.

LaTeX

$$$\text{homEquiv}$ natural in both arguments: \ (adj.homEquiv A_1.a A_1.a) A_1.str \; \circ \; G.map f.f = f.f \; \circ \; (adj.homEquiv A_2.a A_2.a) A_2.str$$$

Lean4

theorem homEquiv_naturality_str (adj : F ⊣ G) (A₁ A₂ : Algebra F) (f : A₁ ⟶ A₂) :
    (adj.homEquiv A₁.a A₁.a) A₁.str ≫ G.map f.f = f.f ≫ (adj.homEquiv A₂.a A₂.a) A₂.str := by
  rw [← Adjunction.homEquiv_naturality_right, ← Adjunction.homEquiv_naturality_left, f.h]

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