equivalenceUnitIso_eq — Mathlib

English

The unit isomorphism of the equivalence is equal to the corresponding unit iso associated to a given equivalence data.

Русский

Единичная изоморфия эквивалентности равна соответствующей единичной изоморфии для данных эквивалентности.

LaTeX

$$$ (\\text{equivalence} \\, hF).\\text{unitIso} = \\text{equivalenceUnitIso} \\, hF $$$

Lean4

theorem equivalenceUnitIso_eq (hε : υ hF = ε) : (equivalence hF hG).unitIso = equivalenceUnitIso hG ε :=
  by
  ext1; apply NatTrans.ext; ext X
  dsimp [equivalence]
  simp only [assoc, comp_id, equivalenceUnitIso_hom_app, equivalence₂_inverse, Functor.comp_obj, id_comp,
    equivalence₂UnitIso_eq eB hF, equivalence₂UnitIso_hom_app, ← eA.inverse.map_comp_assoc, assoc, ← hε, υ_hom_app]

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