rightAdjointCommShift — Mathlib

Lean4
/-- Given an adjunction `F ⊣ G` and a `CommShift` structure on `F`, this constructs
the unique compatible `CommShift` structure on `G`.
-/
@[simps]
noncomputable def rightAdjointCommShift [F.CommShift A] : G.CommShift A
    where
  iso a := iso adj a
  zero :=
    by
    refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso 0) _ _ (compatibilityUnit_iso adj 0) ?_
    rw [F.commShiftIso_zero]
    exact CommShift.compatibilityUnit_isoZero adj
  add a
    b :=
    by
    refine
      CommShift.compatibilityUnit_unique_right adj (F.commShiftIso (a + b)) _ _ (compatibilityUnit_iso adj (a + b)) ?_
    rw [F.commShiftIso_add]
    exact CommShift.compatibilityUnit_isoAdd adj _ _ _ _ (compatibilityUnit_iso adj a) (compatibilityUnit_iso adj b)
Похожие утверждения