isUnital_leftAdd — Mathlib

English

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

Русский

IsUnital_leftAdd задаёт условие безусловности Эккмана—Хильтона для левого сложения; конкретно левый единичный элемент равен 0.

LaTeX

$$$\text{isUnital_leftAdd } X Y$$$

Lean4

theorem isUnital_leftAdd : EckmannHilton.IsUnital (· +ₗ ·) 0 :=
  by
  have hr : ∀ f : X ⟶ Y, biprod.lift (0 : X ⟶ Y) f = f ≫ biprod.inr :=
    by
    intro f
    ext
    · simp
    · simp [Category.assoc]
  have hl : ∀ f : X ⟶ Y, biprod.lift f (0 : X ⟶ Y) = f ≫ biprod.inl :=
    by
    intro f
    ext
    · simp
    · simp [biprod.lift_snd, Category.assoc, comp_zero]
  exact
    { left_id := fun f => by simp [hr f, leftAdd, Category.assoc, Category.comp_id, biprod.inr_desc],
      right_id := fun f => by simp [hl f, leftAdd, Category.assoc, Category.comp_id, biprod.inl_desc] }

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