English
The pushout cocone constructed from the tensor product is a colimit cone; i.e., the pushout of the two maps is universal for commuting diagrams.
Русский
Кокон пуш-аут образует колимит: любой диаграмме, совмещающей отображения, существует единственный канонический морфизм.
LaTeX
$$$\text{pushoutCoconeIsColimit}(R,A,B) : IsColimit(\text{pushoutCocone } R A B)$$$
Lean4
/-- Verify that the `pushout_cocone` is indeed the colimit. -/
def pushoutCoconeIsColimit : Limits.IsColimit (pushoutCocone R A B) :=
Limits.PushoutCocone.isColimitAux' _ fun s =>
by
letI := RingHom.toAlgebra (s.inl.hom.comp (algebraMap R A))
let f' : A →ₐ[R] s.pt := { s.inl.hom with commutes' := fun r => rfl }
let g' : B →ₐ[R] s.pt :=
{ s.inr.hom with
commutes' :=
DFunLike.congr_fun <|
congrArg Hom.hom
((s.ι.naturality Limits.WalkingSpan.Hom.snd).trans (s.ι.naturality Limits.WalkingSpan.Hom.fst).symm) }
letI : Algebra R (pushoutCocone R A B).pt :=
show Algebra R (A ⊗[R] B) by
infer_instance
-- The factor map is a ⊗ b ↦ f(a) * g(b).
use ofHom (AlgHom.toRingHom (Algebra.TensorProduct.productMap f' g'))
simp only [pushoutCocone_inl, pushoutCocone_inr]
constructor
· ext x
exact Algebra.TensorProduct.productMap_left_apply (A := A) _ _ x
constructor
· ext x
exact Algebra.TensorProduct.productMap_right_apply (B := B) _ _ x
intro h eq1 eq2
let h' : A ⊗[R] B →ₐ[R] s.pt :=
{ h.hom with
commutes' := fun r => by
change h (algebraMap R A r ⊗ₜ[R] 1) = s.inl (algebraMap R A r)
rw [← eq1]
simp only [pushoutCocone_pt, coe_of]
rfl }
suffices h' = Algebra.TensorProduct.productMap f' g' by
ext x
change h' x = Algebra.TensorProduct.productMap f' g' x
rw [this]
apply Algebra.TensorProduct.ext'
intro a b
simp only [f', g', ← eq1, pushoutCocone_pt, ← eq2, AlgHom.toRingHom_eq_coe,
Algebra.TensorProduct.productMap_apply_tmul, AlgHom.coe_mk]
change _ = h (a ⊗ₜ 1) * h (1 ⊗ₜ b)
rw [← h.hom.map_mul, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
rfl
