Under CommRingCat

In this file we provide basic API for Under R when R : CommRingCat. Under R is (equivalent to) the category of commutative R-algebras. For not necessarily commutative algebras, use AlgCat R instead.

@[instance_reducible]

instance CommRingCat.instCoeSortUnderType {R : CommRingCat} : CoeSort (CategoryTheory.Under R) (Type u)

Equations

• CommRingCat.instCoeSortUnderType = { coe := fun (A : CategoryTheory.Under R) => ↑A.right }

@[instance_reducible]

instance CommRingCat.instAlgebraCarrierRight {R : CommRingCat} (A : CategoryTheory.Under R) : Algebra ↑R ↑A.right

Equations

• CommRingCat.instAlgebraCarrierRight A = (CommRingCat.Hom.hom A.hom).toAlgebra

def CommRingCat.toAlgHom {R : CommRingCat} {A B : CategoryTheory.Under R} (f : A ⟶ B) : ↑A.right →ₐ[↑R] ↑B.right

Turn a morphism in Under R into an algebra homomorphism.

Equations

• CommRingCat.toAlgHom f = { toRingHom := CommRingCat.Hom.hom (CategoryTheory.Under.Hom.right f), commutes' := ⋯ }

@[simp]

theorem CommRingCat.toAlgHom_id {R : CommRingCat} (A : CategoryTheory.Under R) : toAlgHom (CategoryTheory.CategoryStruct.id A) = AlgHom.id ↑R ↑A.right

@[simp]

theorem CommRingCat.toAlgHom_comp {R : CommRingCat} {A B C : CategoryTheory.Under R} (f : A ⟶ B) (g : B ⟶ C) : toAlgHom (CategoryTheory.CategoryStruct.comp f g) = (toAlgHom g).comp (toAlgHom f)

@[simp]

theorem CommRingCat.toAlgHom_apply {R : CommRingCat} {A B : CategoryTheory.Under R} (f : A ⟶ B) (a : ↑A.right) : (toAlgHom f) a = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f)) a

@[implicit_reducible]

def CommRingCat.mkUnder (R : CommRingCat) (A : Type u) [CommRing A] [Algebra (↑R) A] : CategoryTheory.Under R

Make an object of Under R from an R-algebra.

Equations

• R.mkUnder A = CategoryTheory.Under.mk (CommRingCat.ofHom (algebraMap (↑R) A))

@[simp]

theorem CommRingCat.mkUnder_hom (R : CommRingCat) (A : Type u) [CommRing A] [Algebra (↑R) A] : (R.mkUnder A).hom = ofHom (algebraMap (↑R) A)

theorem CommRingCat.mkUnder_right (R : CommRingCat) (A : Type u) [CommRing A] [Algebra (↑R) A] : (R.mkUnder A).right = ↧A

theorem CommRingCat.mkUnder_ext {R : CommRingCat} {A : Type u} [CommRing A] [Algebra (↑R) A] {B : CategoryTheory.Under R} {f g : R.mkUnder A ⟶ B} (h : ∀ (a : A), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f)) a = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right g)) a) : f = g

theorem CommRingCat.mkUnder_ext_iff {R : CommRingCat} {A : Type u} [CommRing A] [Algebra (↑R) A] {B : CategoryTheory.Under R} {f g : R.mkUnder A ⟶ B} : f = g ↔ ∀ (a : A), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f)) a = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right g)) a

def AlgHom.toUnder {R : CommRingCat} {A B : Type u} [CommRing A] [CommRing B] [Algebra (↑R) A] [Algebra (↑R) B] (f : A →ₐ[↑R] B) : R.mkUnder A ⟶ R.mkUnder B

Make a morphism in Under R from an algebra map.

Equations

• f.toUnder = CategoryTheory.Under.homMk (CommRingCat.ofHom f.toRingHom) ⋯

@[simp]

theorem AlgHom.toUnder_right {R : CommRingCat} {A B : Type u} [CommRing A] [CommRing B] [Algebra (↑R) A] [Algebra (↑R) B] (f : A →ₐ[↑R] B) (a : A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f.toUnder)) a = f a

@[simp]

theorem AlgHom.toUnder_comp {R : CommRingCat} {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra (↑R) A] [Algebra (↑R) B] [Algebra (↑R) C] (f : A →ₐ[↑R] B) (g : B →ₐ[↑R] C) : (g.comp f).toUnder = CategoryTheory.CategoryStruct.comp f.toUnder g.toUnder

def AlgEquiv.toUnder {R : CommRingCat} {A B : Type u} [CommRing A] [CommRing B] [Algebra (↑R) A] [Algebra (↑R) B] (f : A ≃ₐ[↑R] B) : R.mkUnder A ≅ R.mkUnder B

Make an isomorphism in Under R from an algebra isomorphism.

Equations

• f.toUnder = { hom := (↑f).toUnder, inv := (↑f.symm).toUnder, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem AlgEquiv.toUnder_hom_right_apply {R : CommRingCat} {A B : Type u} [CommRing A] [CommRing B] [Algebra (↑R) A] [Algebra (↑R) B] (f : A ≃ₐ[↑R] B) (a : A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f.toUnder.hom)) a = f a

@[simp]

theorem AlgEquiv.toUnder_inv_right_apply {R : CommRingCat} {A B : Type u} [CommRing A] [CommRing B] [Algebra (↑R) A] [Algebra (↑R) B] (f : A ≃ₐ[↑R] B) (b : B) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f.toUnder.inv)) b = f.symm b

@[simp]

theorem AlgEquiv.toUnder_trans {R : CommRingCat} {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra (↑R) A] [Algebra (↑R) B] [Algebra (↑R) C] (f : A ≃ₐ[↑R] B) (g : B ≃ₐ[↑R] C) : (f.trans g).toUnder = f.toUnder ≪≫ g.toUnder

def CommRingCat.tensorProd (R S : CommRingCat) [Algebra ↑R ↑S] : CategoryTheory.Functor (CategoryTheory.Under R) (CategoryTheory.Under S)

The base change functor A ↦ S ⊗[R] A.

Equations

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

@[simp]

theorem CommRingCat.tensorProd_map_right (R S : CommRingCat) [Algebra ↑R ↑S] {X✝ Y✝ : CategoryTheory.Under R} (f : X✝ ⟶ Y✝) : ((R.tensorProd S).map f).right = ofHom ↑(Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f))

@[simp]

theorem CommRingCat.tensorProd_obj_right (R S : CommRingCat) [Algebra ↑R ↑S] (A : CategoryTheory.Under R) : ((R.tensorProd S).obj A).right = ↧(TensorProduct ↑R ↑S ↑A.right)

noncomputable def CommRingCat.tensorProdObjIsoPushoutObj {R : CommRingCat} (S : CommRingCat) [Algebra ↑R ↑S] (A : CategoryTheory.Under R) : S.mkUnder (TensorProduct ↑R ↑S ↑A.right) ≅ (CategoryTheory.Under.pushout (ofHom (algebraMap ↑R ↑S))).obj A

The natural isomorphism S ⊗[R] A ≅ pushout A.hom (algebraMap R S) in Under S.

Equations

• CommRingCat.tensorProdObjIsoPushoutObj S A = CategoryTheory.Under.isoMk ⋯.isoPushout ⋯

@[simp]

theorem CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right {R S : CommRingCat} [Algebra ↑R ↑S] (A : CategoryTheory.Under R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom (ofHom (algebraMap ↑R ↑S))) (CategoryTheory.Under.Hom.right (tensorProdObjIsoPushoutObj S A).inv) = ofHom Algebra.TensorProduct.includeRight.toRingHom

@[simp]

theorem CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc {R S : CommRingCat} [Algebra ↑R ↑S] (A : CategoryTheory.Under R) {Z : CommRingCat} (h : (S.mkUnder (TensorProduct ↑R ↑S ↑A.right)).right ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom (ofHom (algebraMap ↑R ↑S))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right (tensorProdObjIsoPushoutObj S A).inv) h) = CategoryTheory.CategoryStruct.comp (ofHom Algebra.TensorProduct.includeRight.toRingHom) h

@[simp]

theorem CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right {R S : CommRingCat} [Algebra ↑R ↑S] (A : CategoryTheory.Under R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr A.hom (ofHom (algebraMap ↑R ↑S))) (CategoryTheory.Under.Hom.right (tensorProdObjIsoPushoutObj S A).inv) = ofHom Algebra.TensorProduct.includeLeftRingHom

@[simp]

theorem CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc {R S : CommRingCat} [Algebra ↑R ↑S] (A : CategoryTheory.Under R) {Z : CommRingCat} (h : (S.mkUnder (TensorProduct ↑R ↑S ↑A.right)).right ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr A.hom (ofHom (algebraMap ↑R ↑S))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right (tensorProdObjIsoPushoutObj S A).inv) h) = CategoryTheory.CategoryStruct.comp (ofHom Algebra.TensorProduct.includeLeftRingHom) h

noncomputable def CommRingCat.tensorProdIsoPushout (R S : CommRingCat) [Algebra ↑R ↑S] : R.tensorProd S ≅ CategoryTheory.Under.pushout (ofHom (algebraMap ↑R ↑S))

A ↦ S ⊗[R] A is naturally isomorphic to A ↦ pushout A.hom (algebraMap R S).

Equations

• R.tensorProdIsoPushout S = CategoryTheory.NatIso.ofComponents (fun (A : CategoryTheory.Under R) => CommRingCat.tensorProdObjIsoPushoutObj S A) ⋯

@[simp]

theorem CommRingCat.tensorProdIsoPushout_app {R S : CommRingCat} [Algebra ↑R ↑S] (A : CategoryTheory.Under R) : (R.tensorProdIsoPushout S).app A = tensorProdObjIsoPushoutObj S A