leftAdjointCommShift — Mathlib

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