feat(algebra/*): Tensor product is the fibered coproduct in CommRing (#…

…9338)




Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>

src/algebra/category/CommRing/pushout.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2020 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import category_theory.limits.shapes.pullbacks
+import ring_theory.tensor_product
+import algebra.category.CommRing.basic
+
+/-!
+# Explicit pushout cocone for CommRing
+
+In this file we prove that tensor product is indeed the fibered coproduct in `CommRing`, and
+provide the explicit pushout cocone.
+
+-/
+
+universe u
+
+open category_theory
+open_locale tensor_product
+
+variables {R A B : CommRing.{u}} (f : R ⟶ A) (g : R ⟶ B)
+
+namespace CommRing
+
+/-- The explicit cocone with tensor products as the fibered product in `CommRing`. -/
+def pushout_cocone : limits.pushout_cocone f g :=
+begin
+  letI := ring_hom.to_algebra f,
+  letI := ring_hom.to_algebra g,
+  apply limits.pushout_cocone.mk,
+  show CommRing, from CommRing.of (A ⊗[R] B),
+  show A ⟶ _,  from algebra.tensor_product.include_left.to_ring_hom,
+  show B ⟶ _,  from algebra.tensor_product.include_right.to_ring_hom,
+  ext r,
+  transitivity algebra_map R (A ⊗[R] B) r,
+  exact algebra.tensor_product.include_left.commutes r,
+  exact (algebra.tensor_product.include_right.commutes r).symm,
+end
+
+@[simp]
+lemma pushout_cocone_inl : (pushout_cocone f g).inl = (by {
+  letI := f.to_algebra, letI := g.to_algebra,
+  exactI algebra.tensor_product.include_left.to_ring_hom
+}) := rfl
+
+@[simp]
+lemma pushout_cocone_inr : (pushout_cocone f g).inr = (by {
+  letI := f.to_algebra, letI := g.to_algebra,
+  exactI algebra.tensor_product.include_right.to_ring_hom
+}) := rfl
+
+@[simp]
+lemma pushout_cocone_X : (pushout_cocone f g).X = (by {
+  letI := f.to_algebra, letI := g.to_algebra,
+  exactI CommRing.of (A ⊗[R] B)
+}) := rfl
+
+/-- Verify that the `pushout_cocone` is indeed the colimit. -/
+def pushout_cocone_is_colimit : limits.is_colimit (pushout_cocone f g) :=
+limits.pushout_cocone.is_colimit_aux' _ (λ s,
+begin
+  letI := ring_hom.to_algebra f,
+  letI := ring_hom.to_algebra g,
+  letI := ring_hom.to_algebra (f ≫ s.inl),
+  let f' : A →ₐ[R] s.X := { commutes' := λ r, by {
+        change s.inl.to_fun (f r) = (f ≫ s.inl) r, refl
+      }, ..s.inl },
+  let g' : B →ₐ[R] s.X := { commutes' := λ r, by {
+        change (g ≫ s.inr) r = (f ≫ s.inl) r,
+        congr' 1,
+        exact (s.ι.naturality limits.walking_span.hom.snd).trans
+          (s.ι.naturality limits.walking_span.hom.fst).symm
+      }, ..s.inr },
+  /- The factor map is a ⊗ b ↦ f(a) * g(b). -/
+  use alg_hom.to_ring_hom (algebra.tensor_product.product_map f' g'),
+  simp only [pushout_cocone_inl, pushout_cocone_inr],
+  split, { ext x, exact algebra.tensor_product.product_map_left_apply  _ _ x, },
+  split, { ext x, exact algebra.tensor_product.product_map_right_apply _ _ x, },
+  intros h eq1 eq2,
+  let h' : (A ⊗[R] B) →ₐ[R] s.X :=
+    { commutes' := λ r, by {
+      change h ((f r) ⊗ₜ[R] 1) = s.inl (f r),
+      rw ← eq1, simp }, ..h },
+  suffices : h' = algebra.tensor_product.product_map f' g',
+    { ext x,
+      change h' x = algebra.tensor_product.product_map f' g' x,
+      rw this },
+  apply algebra.tensor_product.ext,
+  intros a b,
+  simp [← eq1, ← eq2, ← h.map_mul],
+end)
+
+end CommRing

src/ring_theory/tensor_product.lean

@@ -693,6 +693,12 @@ alg_hom_of_linear_map_tensor_product
   map f g (a ⊗ₜ c) = f a ⊗ₜ g c :=
 rfl
 
+@[simp] lemma map_comp_include_left (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
+  (map f g).comp include_left = include_left.comp f := alg_hom.ext $ by simp
+
+@[simp] lemma map_comp_include_right (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
+  (map f g).comp include_right = include_right.comp g := alg_hom.ext $ by simp
+
 /--
 Construct an isomorphism between tensor products of R-algebras
 from isomorphisms between the tensor factors.
@@ -714,6 +720,51 @@ end
 
 end monoidal
 
-end tensor_product
+section
+
+variables {R A B S : Type*} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S]
+variables [algebra R A] [algebra R B] [algebra R S]
+variables (f : A →ₐ[R] S) (g : B →ₐ[R] S)
+
+variables (R)
+
+/-- `algebra.lmul'` is an alg_hom on commutative rings. -/
+def lmul' : S ⊗[R] S →ₐ[R] S :=
+alg_hom_of_linear_map_tensor_product (algebra.lmul' R)
+  (λ a₁ a₂ b₁ b₂, by simp only [algebra.lmul'_apply, mul_mul_mul_comm])
+  (λ r, by simp only [algebra.lmul'_apply, _root_.mul_one])
+
+variables {R}
+
+lemma lmul'_to_linear_map : (lmul' R : _ →ₐ[R] S).to_linear_map = algebra.lmul' R := rfl
+
+@[simp] lemma lmul'_apply_tmul (a b : S) : lmul' R (a ⊗ₜ[R] b) = a * b := lmul'_apply
+
+@[simp]
+lemma lmul'_comp_include_left : (lmul' R : _ →ₐ[R] S).comp include_left = alg_hom.id R S :=
+alg_hom.ext $ λ _, (lmul'_apply_tmul _ _).trans (_root_.mul_one _)
 
+@[simp]
+lemma lmul'_comp_include_right : (lmul' R : _ →ₐ[R] S).comp include_right = alg_hom.id R S :=
+alg_hom.ext $ λ _, (lmul'_apply_tmul _ _).trans (_root_.one_mul _)
+
+/--
+If `S` is commutative, for a pair of morphisms `f : A →ₐ[R] S`, `g : B →ₐ[R] S`,
+We obtain a map `A ⊗[R] B →ₐ[R] S` that commutes with `f`, `g` via `a ⊗ b ↦ f(a) * g(b)`.
+-/
+def product_map : A ⊗[R] B →ₐ[R] S := (lmul' R).comp (tensor_product.map f g)
+
+@[simp] lemma product_map_apply_tmul (a : A) (b : B) : product_map f g (a ⊗ₜ b) = f a * g b :=
+by { unfold product_map lmul', simp }
+
+lemma product_map_left_apply (a : A) : product_map f g (include_left a) = f a := by simp
+
+@[simp] lemma product_map_left : (product_map f g).comp include_left = f := alg_hom.ext $ by simp
+
+lemma product_map_right_apply (b : B) : product_map f g (include_right b) = g b := by simp
+
+@[simp] lemma product_map_right : (product_map f g).comp include_right = g := alg_hom.ext $ by simp
+
+end
+end tensor_product
 end algebra