Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Ring

Yoneda embedding of RingCatObj C #

source
def CategoryTheory.yonedaRingObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : C) [RingObj R] :
Functor Cᵒᵖ RingCat

If R is a ring object, then Hom(-, R) is a presheaf of rings.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.yonedaRingObj_obj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : C) [RingObj R] (X : Cᵒᵖ) :
    (yonedaRingObj R).obj X = RingCat.of (Opposite.unop X ⟶ R)
    source
    @[simp]
    theorem CategoryTheory.yonedaRingObj_map_apply {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R : C} [RingObj R] {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : Opposite.unop X ⟶ R) :
    (ConcreteCategory.hom ((yonedaRingObj R).map f)) x = CategoryStruct.comp f.unop x
    source
    def CategoryTheory.yonedaRing {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
    Functor (RingObjCat C) (Functor Cᵒᵖ RingCat)

    The yoneda embedding of RingObjCat C into presheaves of rings.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.yonedaCommRingObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : C) [CommRingObj R] :
      Functor Cᵒᵖ CommRingCat

      If R is a commutative ring object, then Hom(-, R) is a presheaf of commutative rings.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.yonedaCommRingObj_obj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : C) [CommRingObj R] (X : Cᵒᵖ) :
        (yonedaCommRingObj R).obj X = CommRingCat.of (Opposite.unop X ⟶ R)
        source
        @[simp]
        theorem CategoryTheory.yonedaCommRingObj_map_apply {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R : C} [CommRingObj R] {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : Opposite.unop X ⟶ R) :
        (ConcreteCategory.hom ((yonedaCommRingObj R).map f)) x = CategoryStruct.comp f.unop x
        source
        def CategoryTheory.yonedaCommRing {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
        Functor (CommRingObjCat C) (Functor Cᵒᵖ CommRingCat)

        The yoneda embedding of CommRingObjCat C into presheaves of commutative rings.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.yonedaCommRing_obj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : CommRingObjCat C) :
          yonedaCommRing.obj R = yonedaCommRingObj R.X
          source
          @[simp]
          theorem CategoryTheory.yonedaCommRing_map_app_apply {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R₁ R₂ : CommRingObjCat C} (f : R₁ ⟶ R₂) {X : C} (x : X ⟶ R₁.X) :
          (ConcreteCategory.hom ((yonedaCommRing.map f).app (Opposite.op X))) x = CategoryStruct.comp x f.hom