compatibilityUnit_isoZero — Mathlib

English

The canonical isomorphisms isoZero for F and G are compatible with the unit of the adjunction.

Русский

Канонические изоморфизмы isoZero для F и G совместимы с единицей сопряжения.

LaTeX

$$$ CompatUnit(adj, \mathrm{isoZero}(F,A), \mathrm{isoZero}(G,A))$$$

Lean4

/-- The isomorphisms `Functor.CommShift.isoZero F` and `Functor.CommShift.isoZero G` are
compatible with the unit of an adjunction `F ⊣ G`.
-/
theorem compatibilityUnit_isoZero :
    CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A) :=
  by
  intro
  simp only [Functor.id_obj, Functor.comp_obj, Functor.CommShift.isoZero_hom_app, Functor.map_comp, assoc,
    unit_naturality_assoc, ← cancel_mono ((shiftFunctorZero C A).hom.app _), ← G.map_comp_assoc, Iso.inv_hom_id_app,
    Functor.id_obj, Functor.map_id, id_comp, NatTrans.naturality, Functor.id_map, assoc, comp_id]

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