HepLean 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
        • X.instSemiring = X.str
        instance SemiRingCat.instFunLike {X Y : SemiRingCat} :
        FunLike (X Y) X Y
        Equations
        • SemiRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
        instance SemiRingCat.instRingHomClass {X Y : SemiRingCat} :
        RingHomClass (X Y) X Y
        Equations
        • =
        theorem SemiRingCat.coe_comp {X Y Z : SemiRingCat} {f : X Y} {g : Y Z} :
        @[simp]
        theorem SemiRingCat.ext {X Y : SemiRingCat} {f 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 Y Z : Type u} [Semiring X] [Semiring Y] [Semiring Z] (f : X →+* Y) (g : Y →+* Z) :
          (CategoryTheory.CategoryStruct.comp f g) = (g.comp f)
          @[simp]

          Variant of SemiRingCat.coe_comp_of for morphisms.

          theorem SemiRingCat.ext_of {X Y : Type u} [Semiring X] [Semiring Y] (f g : X →+* Y) (h : ∀ (x : X), f x = g x) :
          f = g
          @[simp]
          theorem SemiRingCat.RingEquiv_coe_eq {X 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 S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x : R) :
            @[simp]
            theorem SemiRingCat.ofHom_apply' {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x : R) :

            A variant of ofHom_apply that makes simpNF happy

            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
              @[simp]
              theorem RingEquiv.toSemiRingCatIso_inv {X Y : Type u} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
              e.toSemiRingCatIso.inv = e.symm.toRingHom
              @[simp]
              theorem RingEquiv.toSemiRingCatIso_hom {X Y : Type u} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
              e.toSemiRingCatIso.hom = e.toRingHom
              @[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
                instance RingCat.instRing (X : RingCat) :
                Ring X
                Equations
                • X.instRing = X.str
                instance RingCat.instFunLike {X Y : RingCat} :
                FunLike (X Y) X Y
                Equations
                • RingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
                instance RingCat.instRingHomClass {X Y : RingCat} :
                RingHomClass (X Y) X Y
                Equations
                • =
                theorem RingCat.coe_comp {X Y Z : RingCat} {f : X Y} {g : Y Z} :
                @[simp]
                theorem RingCat.forget_map {X Y : RingCat} (f : X Y) :
                theorem RingCat.ext {X Y : RingCat} {f 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 S : Type u} [Ring R] [Ring S] (f : R →+* S) :

                  Typecheck a RingHom as a morphism in RingCat.

                  Equations
                  Instances For
                    theorem RingCat.ofHom_apply {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (x : R) :
                    (RingCat.ofHom f) x = f x
                    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.ofHom_apply' {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (x : R) :
                    (RingCat.ofHom f) x = f x

                    A variant of ofHom_apply that makes simpNF happy

                    @[simp]
                    theorem RingCat.coe_comp_of {X Y Z : Type u} [Ring X] [Ring Y] [Ring Z] (f : X →+* Y) (g : Y →+* Z) :
                    (CategoryTheory.CategoryStruct.comp f g) = (g.comp f)
                    @[simp]
                    theorem RingCat.coe_comp_of' {X Z : Type u} {Y : RingCat} [Ring X] [Ring Z] (f : RingCat.of X Y) (g : Y RingCat.of Z) :

                    Variant of RingCat.coe_comp_of for morphisms.

                    theorem RingCat.ext_of {X Y : Type u} [Ring X] [Ring Y] (f g : X →+* Y) (h : ∀ (x : X), f x = g x) :
                    f = g
                    @[simp]
                    theorem RingCat.RingEquiv_coe_eq {X 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.
                    @[reducible, inline]
                    abbrev CommSemiRingCat :
                    Type (u + 1)

                    The category of commutative semirings.

                    Equations
                    Instances For
                      Equations
                      • X.instCommSemiringα = X.str
                      Equations
                      • X.instCommSemiring = X.str
                      instance CommSemiRingCat.instFunLike {X Y : CommSemiRingCat} :
                      FunLike (X Y) X Y
                      Equations
                      • CommSemiRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
                      Equations
                      • =
                      theorem CommSemiRingCat.coe_comp {X Y Z : CommSemiRingCat} {f : X Y} {g : Y Z} :
                      theorem CommSemiRingCat.ext {X Y : CommSemiRingCat} {f 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 Y : Type u_1} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
                          e = e
                          theorem CommSemiRingCat.ofHom_apply {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : R) :
                          @[simp]
                          theorem CommSemiRingCat.ofHom_apply' {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : R) :

                          A variant of ofHom_apply that makes simpNF happy

                          Equations
                          • R.instCommSemiringα_1 = R.str
                          @[simp]
                          @[simp]
                          theorem CommSemiRingCat.coe_comp_of {X Y 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 Y : Type u} [CommSemiring X] [CommSemiring Y] (f 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.

                          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
                            @[simp]
                            theorem RingEquiv.toCommSemiRingCatIso_hom {X Y : Type u} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
                            e.toCommSemiRingCatIso.hom = e.toRingHom
                            @[simp]
                            theorem RingEquiv.toCommSemiRingCatIso_inv {X Y : Type u} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
                            e.toCommSemiRingCatIso.inv = e.symm.toRingHom
                            @[reducible, inline]
                            abbrev CommRingCat :
                            Type (u + 1)

                            The category of commutative rings.

                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Equations
                              • X.instCommRing = X.str
                              Equations
                              • X.instCommRing' = X.str
                              instance CommRingCat.instFunLike {X Y : CommRingCat} :
                              FunLike (X Y) X Y
                              Equations
                              • CommRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
                              instance CommRingCat.instRingHomClass {X Y : CommRingCat} :
                              RingHomClass (X Y) X Y
                              Equations
                              • =
                              theorem CommRingCat.coe_comp {X Y 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.comp_apply {R S T : CommRingCat} (f : R S) (g : S T) (x : R) :
                              @[simp]
                              theorem CommRingCat.ext {X Y : CommRingCat} {f 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 Y : Type u_1} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
                                  e = e
                                  theorem CommRingCat.ofHom_apply {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (x : R) :
                                  @[simp]
                                  theorem CommRingCat.ofHom_apply' {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (x : R) :

                                  A variant of ofHom_apply that makes simpNF happy

                                  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 Y Z : Type u} [CommRing X] [CommRing Y] [CommRing Z] (f : X →+* Y) (g : Y →+* Z) :
                                  (CategoryTheory.CategoryStruct.comp f g) = (g.comp f)
                                  @[simp]

                                  Variant of CommRingCat.coe_comp_of for morphisms.

                                  theorem CommRingCat.ext_of {X Y : Type u} [CommRing X] [CommRing Y] (f g : X →+* Y) (h : ∀ (x : X), f x = g x) :
                                  f = g
                                  @[simp]

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

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  def RingEquiv.toRingCatIso {X 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.toRingCatIso_hom {X Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) :
                                    e.toRingCatIso.hom = e.toRingHom
                                    @[simp]
                                    theorem RingEquiv.toRingCatIso_inv {X Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) :
                                    e.toRingCatIso.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
                                      @[simp]
                                      theorem RingEquiv.toCommRingCatIso_inv {X Y : Type u} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
                                      e.toCommRingCatIso.inv = e.symm.toRingHom
                                      @[simp]
                                      theorem RingEquiv.toCommRingCatIso_hom {X Y : Type u} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
                                      e.toCommRingCatIso.hom = e.toRingHom

                                      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 Y : CommRingCat} (i : X Y) :
                                          i.commRingCatIsoToRingEquiv.toRingHom = i.hom
                                          @[simp]
                                          theorem CategoryTheory.Iso.commRingIsoToRingEquiv_symm_toRingHom {X Y : CommRingCat} (i : X Y) :
                                          i.commRingCatIsoToRingEquiv.symm.toRingHom = i.inv
                                          @[simp]
                                          theorem CategoryTheory.Iso.commRingIsoToRingEquiv_apply {X Y : CommRingCat} (i : X Y) (x : X) :
                                          i.commRingCatIsoToRingEquiv x = i.hom x
                                          @[simp]
                                          theorem CategoryTheory.Iso.commRingIsoToRingEquiv_symm_apply {X Y : CommRingCat} (i : X Y) (y : Y) :
                                          i.commRingCatIsoToRingEquiv.symm y = i.inv 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) :