map_map — Mathlib

English

The composition coprod.map coprod.inl coprod.inr followed by codiag equals the identity on the coproduct X ⨿ Y.

Русский

Составление coprod.map coprod.inl coprod.inr затем codiag равно тождественному на X ⨿ Y.

LaTeX

$$$coprod.map coprod.inl coprod.inr \; \circ \; codiag (X \sqcup Y) = id_{X \sqcup Y}$$$

Lean4

@[reassoc (attr := simp)]
theorem map_map {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryCoproduct A₁ B₁] [HasBinaryCoproduct A₂ B₂] [HasBinaryCoproduct A₃ B₃]
    (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) :
    coprod.map f g ≫ coprod.map h k = coprod.map (f ≫ h) (g ≫ k) := by
  ext <;>
    simp
      -- I don't think it's a good idea to make any of the following three simp lemmas.

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