coproductCoconeIsColimit — Mathlib

Lean4
/-- The tensor product `A ⊗[ℤ] B` is a coproduct for `A` and `B`. -/
@[simps]
def coproductCoconeIsColimit : IsColimit (coproductCocone A B)
    where
  desc
    (s :
      BinaryCofan A
        B) :=
    ofHom
      (Algebra.TensorProduct.lift s.inl.hom.toIntAlgHom s.inr.hom.toIntAlgHom
          (fun _ _ => by apply Commute.all)).toRingHom
  fac (s : BinaryCofan A B) := fun ⟨j⟩ => by cases j <;> ext a <;> simp
  uniq
    (s : BinaryCofan A B) := by
    rintro ⟨m : A ⊗[ℤ] B →+* s.pt⟩ hm
    apply CommRingCat.hom_ext
    apply RingHom.toIntAlgHom_injective
    apply Algebra.TensorProduct.liftEquiv.symm.injective
    apply Subtype.ext
    rw [Algebra.TensorProduct.liftEquiv_symm_apply_coe, Prod.mk.injEq]
    constructor
    · ext a
      simp [map_one, mul_one, ← hm (Discrete.mk WalkingPair.left)]
    · ext b
      simp [map_one, ← hm (Discrete.mk WalkingPair.right)]
Похожие утверждения