Documentation

Mathlib.Algebra.Category.Ring.Basic

Category instances for Semiring, Ring, CommSemiring, and CommRing. #

We introduce the bundled categories:

@[reducible, inline]
abbrev SemiRingCat :
Type (u + 1)

The category of semirings.

Equations
Instances For
    @[reducible, inline]
    abbrev SemiRingCatMax :
    Type ((max u1 u2) + 1)

    An alias for Semiring.{max u v}, to deal around unification issues.

    Equations
    Instances For
      @[reducible, inline]
      abbrev SemiRingCat.AssocRingHom (M : Type u_1) (N : Type u_2) [Semiring M] [Semiring N] :
      Type (max u_1 u_2)

      RingHom doesn't actually assume associativity. This alias is needed to make the category theory machinery work. We use the same trick in MonCat.AssocMonoidHom.

      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        Instances For
          Equations
          • X.instSemiring = X.str
          instance SemiRingCat.instFunLike {X : SemiRingCat} {Y : SemiRingCat} :
          FunLike (X Y) X Y
          Equations
          • SemiRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
          Equations
          • =
          theorem SemiRingCat.coe_comp {X : SemiRingCat} {Y : SemiRingCat} {Z : SemiRingCat} {f : X Y} {g : Y Z} :
          @[simp]
          theorem SemiRingCat.ext {X : SemiRingCat} {Y : SemiRingCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
          f = g

          Construct a bundled SemiRing from the underlying type and typeclass.

          Equations
          Instances For
            @[simp]
            theorem SemiRingCat.coe_of (R : Type u) [Semiring R] :
            (SemiRingCat.of R) = R
            @[simp]
            theorem SemiRingCat.coe_comp_of {X : Type u} {Y : Type u} {Z : Type u} [Semiring X] [Semiring Y] [Semiring Z] (f : X →+* Y) (g : Y →+* Z) :
            (CategoryTheory.CategoryStruct.comp f g) = (g.comp f)
            theorem SemiRingCat.ext_of {X : Type u} {Y : Type u} [Semiring X] [Semiring Y] (f : X →+* Y) (g : X →+* Y) (h : ∀ (x : X), f x = g x) :
            f = g
            @[simp]
            theorem SemiRingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
            e = e
            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            • One or more equations did not get rendered due to their size.

            Typecheck a RingHom as a morphism in SemiRingCat.

            Equations
            Instances For
              @[simp]
              theorem SemiRingCat.ofHom_apply {R : Type u} {S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x : R) :
              @[simp]
              theorem RingEquiv.toSemiRingCatIso_hom {X : Type u} {Y : Type u} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
              e.toSemiRingCatIso.hom = e.toRingHom
              @[simp]
              theorem RingEquiv.toSemiRingCatIso_inv {X : Type u} {Y : Type u} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
              e.toSemiRingCatIso.inv = e.symm.toRingHom

              Ring equivalence are isomorphisms in category of semirings

              Equations
              • e.toSemiRingCatIso = { hom := e.toRingHom, inv := e.symm.toRingHom, hom_inv_id := , inv_hom_id := }
              Instances For
                @[reducible, inline]
                abbrev RingCat :
                Type (u + 1)

                The category of rings.

                Equations
                Instances For
                  instance RingCat.instRingα (X : RingCat) :
                  Ring X
                  Equations
                  • X.instRingα = X.str
                  Equations
                  Instances For
                    instance RingCat.instRing (X : RingCat) :
                    Ring X
                    Equations
                    • X.instRing = X.str
                    instance RingCat.instFunLike {X : RingCat} {Y : RingCat} :
                    FunLike (X Y) X Y
                    Equations
                    • RingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
                    instance RingCat.instRingHomClass {X : RingCat} {Y : RingCat} :
                    RingHomClass (X Y) X Y
                    Equations
                    • =
                    theorem RingCat.coe_comp {X : RingCat} {Y : RingCat} {Z : RingCat} {f : X Y} {g : Y Z} :
                    @[simp]
                    theorem RingCat.forget_map {X : RingCat} {Y : RingCat} (f : X Y) :
                    theorem RingCat.ext {X : RingCat} {Y : RingCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
                    f = g
                    def RingCat.of (R : Type u) [Ring R] :

                    Construct a bundled RingCat from the underlying type and typeclass.

                    Equations
                    Instances For
                      def RingCat.ofHom {R : Type u} {S : Type u} [Ring R] [Ring S] (f : R →+* S) :

                      Typecheck a RingHom as a morphism in RingCat.

                      Equations
                      Instances For
                        instance RingCat.instRingα_1 (R : RingCat) :
                        Ring R
                        Equations
                        • R.instRingα_1 = R.str
                        @[simp]
                        theorem RingCat.coe_of (R : Type u) [Ring R] :
                        (RingCat.of R) = R
                        @[simp]
                        theorem RingCat.coe_comp_of {X : Type u} {Y : Type u} {Z : Type u} [Ring X] [Ring Y] [Ring Z] (f : X →+* Y) (g : Y →+* Z) :
                        (CategoryTheory.CategoryStruct.comp f g) = (g.comp f)
                        theorem RingCat.ext_of {X : Type u} {Y : Type u} [Ring X] [Ring Y] (f : X →+* Y) (g : X →+* Y) (h : ∀ (x : X), f x = g x) :
                        f = g
                        @[simp]
                        theorem RingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [Ring X] [Ring Y] (e : X ≃+* Y) :
                        e = e
                        Equations
                        • One or more equations did not get rendered due to their size.
                        def CommSemiRingCat :
                        Type (u + 1)

                        The category of commutative semirings.

                        Equations
                        Instances For
                          Equations
                          • X.instCommSemiringα = X.str
                          Equations
                          Instances For
                            Equations
                            • X.instCommSemiring = X.str
                            Equations
                            • CommSemiRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
                            Equations
                            • =
                            theorem CommSemiRingCat.ext {X : CommSemiRingCat} {Y : CommSemiRingCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
                            f = g

                            Construct a bundled CommSemiRingCat from the underlying type and typeclass.

                            Equations
                            Instances For

                              Typecheck a RingHom as a morphism in CommSemiRingCat.

                              Equations
                              Instances For
                                @[simp]
                                theorem CommSemiRingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
                                e = e
                                Equations
                                • R.instCommSemiringα_1 = R.str
                                @[simp]
                                @[simp]
                                theorem CommSemiRingCat.coe_comp_of {X : Type u} {Y : Type u} {Z : Type u} [CommSemiring X] [CommSemiring Y] [CommSemiring Z] (f : X →+* Y) (g : Y →+* Z) :
                                (CategoryTheory.CategoryStruct.comp f g) = (g.comp f)
                                theorem CommSemiRingCat.ext_of {X : Type u} {Y : Type u} [CommSemiring X] [CommSemiring Y] (f : X →+* Y) (g : X →+* Y) (h : ∀ (x : X), f x = g x) :
                                f = g

                                The forgetful functor from commutative rings to (multiplicative) commutative monoids.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[simp]
                                theorem RingEquiv.toCommSemiRingCatIso_inv {X : Type u} {Y : Type u} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
                                e.toCommSemiRingCatIso.inv = e.symm.toRingHom
                                @[simp]
                                theorem RingEquiv.toCommSemiRingCatIso_hom {X : Type u} {Y : Type u} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
                                e.toCommSemiRingCatIso.hom = e.toRingHom

                                Ring equivalence are isomorphisms in category of commutative semirings

                                Equations
                                • e.toCommSemiRingCatIso = { hom := e.toRingHom, inv := e.symm.toRingHom, hom_inv_id := , inv_hom_id := }
                                Instances For
                                  def CommRingCat :
                                  Type (u + 1)

                                  The category of commutative rings.

                                  Equations
                                  Instances For
                                    Equations
                                    Instances For
                                      Equations
                                      • X.instCommRing = X.str
                                      Equations
                                      • X.instCommRing' = X.str
                                      instance CommRingCat.instFunLike {X : CommRingCat} {Y : CommRingCat} :
                                      FunLike (X Y) X Y
                                      Equations
                                      • CommRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
                                      Equations
                                      • =
                                      theorem CommRingCat.coe_comp {X : CommRingCat} {Y : CommRingCat} {Z : CommRingCat} {f : X Y} {g : Y Z} :
                                      @[simp]

                                      Specialization of ConcreteCategory.id_apply because simp can't see through the defeq.

                                      @[simp]
                                      theorem CommRingCat.ext {X : CommRingCat} {Y : CommRingCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
                                      f = g

                                      Construct a bundled CommRingCat from the underlying type and typeclass.

                                      Equations
                                      Instances For
                                        instance CommRingCat.instFunLike' {X : Type u_1} [CommRing X] {Y : CommRingCat} :
                                        Equations
                                        • CommRingCat.instFunLike' = CategoryTheory.ConcreteCategory.instFunLike
                                        instance CommRingCat.instFunLike'' {X : CommRingCat} {Y : Type u_1} [CommRing Y] :
                                        FunLike (X CommRingCat.of Y) (X) Y
                                        Equations
                                        • CommRingCat.instFunLike'' = CategoryTheory.ConcreteCategory.instFunLike
                                        Equations
                                        • CommRingCat.instFunLike''' = CategoryTheory.ConcreteCategory.instFunLike

                                        Typecheck a RingHom as a morphism in CommRingCat.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem CommRingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
                                          e = e
                                          Equations
                                          • R.instCommRingα = R.str
                                          @[simp]
                                          theorem CommRingCat.coe_of (R : Type u) [CommRing R] :
                                          (CommRingCat.of R) = R
                                          @[simp]
                                          theorem CommRingCat.coe_comp_of {X : Type u} {Y : Type u} {Z : Type u} [CommRing X] [CommRing Y] [CommRing Z] (f : X →+* Y) (g : Y →+* Z) :
                                          (CategoryTheory.CategoryStruct.comp f g) = (g.comp f)
                                          theorem CommRingCat.ext_of {X : Type u} {Y : Type u} [CommRing X] [CommRing Y] (f : X →+* Y) (g : X →+* Y) (h : ∀ (x : X), f x = g x) :
                                          f = g

                                          The forgetful functor from commutative rings to (multiplicative) commutative monoids.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          @[simp]
                                          theorem RingEquiv.toRingCatIso_hom {X : Type u} {Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) :
                                          e.toRingCatIso.hom = e.toRingHom
                                          @[simp]
                                          theorem RingEquiv.toRingCatIso_inv {X : Type u} {Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) :
                                          e.toRingCatIso.inv = e.symm.toRingHom
                                          def RingEquiv.toRingCatIso {X : Type u} {Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) :

                                          Build an isomorphism in the category RingCat from a RingEquiv between RingCats.

                                          Equations
                                          • e.toRingCatIso = { hom := e.toRingHom, inv := e.symm.toRingHom, hom_inv_id := , inv_hom_id := }
                                          Instances For
                                            @[simp]
                                            theorem RingEquiv.toCommRingCatIso_hom {X : Type u} {Y : Type u} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
                                            e.toCommRingCatIso.hom = e.toRingHom
                                            @[simp]
                                            theorem RingEquiv.toCommRingCatIso_inv {X : Type u} {Y : Type u} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
                                            e.toCommRingCatIso.inv = e.symm.toRingHom

                                            Build an isomorphism in the category CommRingCat from a RingEquiv between CommRingCats.

                                            Equations
                                            • e.toCommRingCatIso = { hom := e.toRingHom, inv := e.symm.toRingHom, hom_inv_id := , inv_hom_id := }
                                            Instances For

                                              Build a RingEquiv from an isomorphism in the category RingCat.

                                              Equations
                                              Instances For

                                                Build a RingEquiv from an isomorphism in the category CommRingCat.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.Iso.commRingIsoToRingEquiv_toRingHom {X : CommRingCat} {Y : CommRingCat} (i : X Y) :
                                                  i.commRingCatIsoToRingEquiv.toRingHom = i.hom
                                                  @[simp]
                                                  theorem CategoryTheory.Iso.commRingIsoToRingEquiv_symm_toRingHom {X : CommRingCat} {Y : CommRingCat} (i : X Y) :
                                                  i.commRingCatIsoToRingEquiv.symm.toRingHom = i.inv
                                                  def ringEquivIsoRingIso {X : Type u} {Y : Type u} [Ring X] [Ring Y] :

                                                  Ring equivalences between RingCats are the same as (isomorphic to) isomorphisms in RingCat.

                                                  Equations
                                                  • ringEquivIsoRingIso = { hom := fun (e : X ≃+* Y) => e.toRingCatIso, inv := fun (i : RingCat.of X RingCat.of Y) => i.ringCatIsoToRingEquiv, hom_inv_id := , inv_hom_id := }
                                                  Instances For

                                                    Ring equivalences between CommRingCats are the same as (isomorphic to) isomorphisms in CommRingCat.

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

                                                      @[simp] lemmas for RingHom.comp and categorical identities.

                                                      @[simp]
                                                      theorem RingHom.comp_id_semiringCat {G : SemiRingCat} {H : Type u} [Semiring H] (f : G →+* H) :
                                                      @[simp]
                                                      theorem RingHom.comp_id_ringCat {G : RingCat} {H : Type u} [Ring H] (f : G →+* H) :
                                                      @[simp]
                                                      @[simp]
                                                      theorem RingHom.comp_id_commRingCat {G : CommRingCat} {H : Type u} [CommRing H] (f : G →+* H) :