The cocartesian monoidal category structure on commutative R-algebras

def CommAlg.binaryCofan {R : Type u} [CommRing R] (A B : CommAlg R) : CategoryTheory.Limits.BinaryCofan A B

The explicit cocone with tensor products as the fibered product in CommAlg.

Equations

• A.binaryCofan B = CategoryTheory.Limits.BinaryCofan.mk (CommAlg.ofHom Algebra.TensorProduct.includeLeft) (CommAlg.ofHom Algebra.TensorProduct.includeRight)

@[simp]

theorem CommAlg.binaryCofan_inl {R : Type u} [CommRing R] (A B : CommAlg R) : (A.binaryCofan B).inl = ofHom Algebra.TensorProduct.includeLeft

@[simp]

theorem CommAlg.binaryCofan_inr {R : Type u} [CommRing R] (A B : CommAlg R) : (A.binaryCofan B).inr = ofHom Algebra.TensorProduct.includeRight

@[simp]

theorem CommAlg.binaryCofan_pt {R : Type u} [CommRing R] (A B : CommAlg R) : (A.binaryCofan B).pt = of R (TensorProduct R ↑A ↑B)

def CommAlg.binaryCofanIsColimit {R : Type u} [CommRing R] (A B : CommAlg R) : CategoryTheory.Limits.IsColimit (A.binaryCofan B)

Verify that the pushout cocone is indeed the colimit.

Equations

• One or more equations did not get rendered due to their size.

def CommAlg.isInitialSelf {R : Type u} [CommRing R] : CategoryTheory.Limits.IsInitial (of R R)

Equations

• CommAlg.isInitialSelf = CategoryTheory.Limits.IsInitial.ofUniqueHom (fun (A : CommAlg R) => CommAlg.ofHom (Algebra.ofId R ↑A)) ⋯

instance CommAlg.instChosenFiniteProductsOpposite {R : Type u} [CommRing R] : CategoryTheory.ChosenFiniteProducts (CommAlg R)ᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

theorem CommAlg.rightWhisker_hom {R : Type u} [CommRing R] {A B : CommAlg R} (C : CommAlg R) (f : A ⟶ B) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.op (Opposite.op C)).unop = Algebra.TensorProduct.map (Hom.hom f) (AlgHom.id R ↑(Opposite.unop (Opposite.op C)))

theorem CommAlg.leftWhisker_hom {R : Type u} [CommRing R] {A B : CommAlg R} (C : CommAlg R) (f : A ⟶ B) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Opposite.op C) f.op).unop = Algebra.TensorProduct.map (AlgHom.id R ↑(Opposite.unop (Opposite.op C))) (Hom.hom f)

theorem CommAlg.associator_hom_unop_hom {R : Type u} [CommRing R] {A B C : CommAlg R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.op A) (Opposite.op B) (Opposite.op C)).hom.unop = ↑(Algebra.TensorProduct.assoc R ↑A ↑B ↑C).symm

theorem CommAlg.associator_inv_unop_hom {R : Type u} [CommRing R] {A B C : CommAlg R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.op A) (Opposite.op B) (Opposite.op C)).inv.unop = ↑(Algebra.TensorProduct.assoc R ↑A ↑B ↑C)

theorem CommAlg.tensorHom_unop_hom {R : Type u} [CommRing R] {A B C D : CommAlg R} (f : A ⟶ C) (g : B ⟶ D) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f.op g.op).unop = Algebra.TensorProduct.map (Hom.hom f) (Hom.hom g)