Documentation

Mathlib.Algebra.Category.Ring.Under.Basic

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.

source
instance CommRingCat.instCoeSortUnderType {R : CommRingCat} :
CoeSort (CategoryTheory.Under R) (Type u)
Equations
    source
    instance CommRingCat.instAlgebraCarrierRightDiscretePUnit {R : CommRingCat} (A : CategoryTheory.Under R) :
    Algebra ↑R ↑A.right
    Equations
      source
      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
        Instances For
          source
          @[simp]
          theorem CommRingCat.toAlgHom_id {R : CommRingCat} (A : CategoryTheory.Under R) :
          toAlgHom (CategoryTheory.CategoryStruct.id A) = AlgHom.id ↑R ↑A.right
          source
          @[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)
          source
          @[simp]
          theorem CommRingCat.toAlgHom_apply {R : CommRingCat} {A B : CategoryTheory.Under R} (f : A ⟶ B) (a : ↑A.right) :
          (toAlgHom f) a = (CategoryTheory.ConcreteCategory.hom f.right) a
          source
          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
            Instances For
              source
              @[simp]
              theorem CommRingCat.mkUnder_hom (R : CommRingCat) (A : Type u) [CommRing A] [Algebra (↑R) A] :
              (R.mkUnder A).hom = ofHom (algebraMap (↑R) A)
              source
              theorem CommRingCat.mkUnder_right (R : CommRingCat) (A : Type u) [CommRing A] [Algebra (↑R) A] :
              (R.mkUnder A).right = of A
              source
              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 f.right) a = (CategoryTheory.ConcreteCategory.hom g.right) a) :
              f = g
              source
              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 f.right) a = (CategoryTheory.ConcreteCategory.hom g.right) a
              source
              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
                Instances For
                  source
                  @[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 f.toUnder.right) a = f a
                  source
                  @[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
                  source
                  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
                    Instances For
                      source
                      @[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 f.toUnder.hom.right) a = f a
                      source
                      @[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 f.toUnder.inv.right) b = f.symm b
                      source
                      @[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
                      source
                      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
                        Instances For
                          source
                          @[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))
                          source
                          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
                            Instances For
                              source
                              @[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))) (tensorProdObjIsoPushoutObj S A).inv.right = ofHom Algebra.TensorProduct.includeRight.toRingHom
                              source
                              @[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 (tensorProdObjIsoPushoutObj S A).inv.right h) = CategoryTheory.CategoryStruct.comp (ofHom Algebra.TensorProduct.includeRight.toRingHom) h
                              source
                              @[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))) (tensorProdObjIsoPushoutObj S A).inv.right = ofHom Algebra.TensorProduct.includeLeftRingHom
                              source
                              @[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 (tensorProdObjIsoPushoutObj S A).inv.right h) = CategoryTheory.CategoryStruct.comp (ofHom Algebra.TensorProduct.includeLeftRingHom) h
                              source
                              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
                                Instances For
                                  source
                                  @[simp]
                                  theorem CommRingCat.tensorProdIsoPushout_app {R S : CommRingCat} [Algebra ↑R ↑S] (A : CategoryTheory.Under R) :
                                  (R.tensorProdIsoPushout S).app A = tensorProdObjIsoPushoutObj S A