isUnital_rightAdd — Mathlib

English

IsUnital_rightAdd expresses the Eckmann–Hilton unitality for the right addition; concretely, (rightAdd X Y) with left addition has a right unit 0.

Русский

IsUnital_rightAdd задаёт условие для правого сложения; правый единичный элемент равен 0.

LaTeX

$$$\text{isUnital_rightAdd } X Y$$$

Lean4

theorem isUnital_rightAdd : EckmannHilton.IsUnital (· +ᵣ ·) 0 :=
  by
  have h₂ : ∀ f : X ⟶ Y, biprod.desc (0 : X ⟶ Y) f = biprod.snd ≫ f :=
    by
    intro f
    ext
    · simp
    · simp only [biprod.inr_desc, BinaryBicone.inr_snd_assoc]
  have h₁ : ∀ f : X ⟶ Y, biprod.desc f (0 : X ⟶ Y) = biprod.fst ≫ f :=
    by
    intro f
    ext
    · simp
    · simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]
  exact
    { left_id := fun f => by simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp],
      right_id := fun f => by simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp] }

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