compatibilityUnit_unique_right — Mathlib

English

If two unit data e1,e1' are compatible with the same right data e2, then e1 = e1'.

Русский

Если две единичные данные e1,e1' совместимы с одним и тем же правым данными e2, то они равны.

LaTeX

$$$ CompatUnit(adj, e_1, e_2) \rightarrow CompatUnit(adj, e_1', e_2) \rightarrow e_1 = e_1'$$$

Lean4

/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
unit of the adjunction `adj`, then `e₁` uniquely determines `e₂`.
-/
theorem compatibilityUnit_unique_right (h : CompatibilityUnit adj e₁ e₂) (h' : CompatibilityUnit adj e₁ e₂') :
    e₂ = e₂' := by
  rw [← Iso.symm_eq_iff]
  ext
  rw [Iso.symm_hom, Iso.symm_hom, compatibilityUnit_right adj e₁ e₂ h, compatibilityUnit_right adj e₁ e₂' h']

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