Documentation

Mathlib.RingTheory.Ideal.Quotient

Ideal quotients #

This file defines ideal quotients as a special case of submodule quotients and proves some basic results about these quotients.

See Algebra.RingQuot for quotients of non-commutative rings.

Main definitions #

@[reducible, inline]

The quotient R/I of a ring R by an ideal I.

The ideal quotient of I is defined to equal the quotient of I as an R-submodule of R. This definition uses abbrev so that typeclass instances can be shared between Ideal.Quotient I and Submodule.Quotient I.

Equations
  • Ideal.instHasQuotient = Submodule.hasQuotient
instance Ideal.Quotient.one {R : Type u} [CommRing R] (I : Ideal R) :
One (R I)
Equations
def Ideal.Quotient.ringCon {R : Type u} [CommRing R] (I : Ideal R) :

On Ideals, Submodule.quotientRel is a ring congruence.

Equations
Instances For
    @[instance 100]
    instance Ideal.Quotient.isScalarTower_right {R : Type u} [CommRing R] {I : Ideal R} {α : Type u_1} [SMul α R] [IsScalarTower α R R] :
    IsScalarTower α (R I) (R I)
    Equations
    • =
    instance Ideal.Quotient.smulCommClass {R : Type u} [CommRing R] {I : Ideal R} {α : Type u_1} [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] :
    SMulCommClass α (R I) (R I)
    Equations
    • =
    instance Ideal.Quotient.smulCommClass' {R : Type u} [CommRing R] {I : Ideal R} {α : Type u_1} [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] :
    SMulCommClass (R I) α (R I)
    Equations
    • =
    def Ideal.Quotient.mk {R : Type u} [CommRing R] (I : Ideal R) :
    R →+* R I

    The ring homomorphism from a ring R to a quotient ring R/I.

    Equations
    Instances For
      instance Ideal.Quotient.instCoeQuotient {R : Type u} [CommRing R] {I : Ideal R} :
      Coe R (R I)
      Equations
      theorem Ideal.Quotient.ringHom_ext_iff {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [NonAssocSemiring S] {f : R I →+* S} {g : R I →+* S} :
      f = g f.comp (Ideal.Quotient.mk I) = g.comp (Ideal.Quotient.mk I)
      theorem Ideal.Quotient.ringHom_ext {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [NonAssocSemiring S] ⦃f : R I →+* S ⦃g : R I →+* S (h : f.comp (Ideal.Quotient.mk I) = g.comp (Ideal.Quotient.mk I)) :
      f = g

      Two RingHoms from the quotient by an ideal are equal if their compositions with Ideal.Quotient.mk' are equal.

      See note [partially-applied ext lemmas].

      instance Ideal.Quotient.inhabited {R : Type u} [CommRing R] {I : Ideal R} :
      Equations
      theorem Ideal.Quotient.eq {R : Type u} [CommRing R] {I : Ideal R} {x : R} {y : R} :
      @[simp]
      theorem Ideal.Quotient.eq_zero_iff_mem {R : Type u} [CommRing R] {a : R} {I : Ideal R} :
      theorem Ideal.Quotient.eq_zero_iff_dvd {R : Type u} [CommRing R] (x : R) (y : R) :
      @[simp]
      theorem Ideal.Quotient.mk_eq_mk_iff_sub_mem {R : Type u} [CommRing R] {I : Ideal R} (x : R) (y : R) :
      theorem Ideal.Quotient.zero_eq_one_iff {R : Type u} [CommRing R] {I : Ideal R} :
      0 = 1 I =
      theorem Ideal.Quotient.nontrivial {R : Type u} [CommRing R] {I : Ideal R} (hI : I ) :
      Equations
      • Ideal.Quotient.instUniqueQuotientTop = { default := 0, uniq := }
      theorem Ideal.Quotient.quotient_ring_saturate {R : Type u} [CommRing R] (I : Ideal R) (s : Set R) :
      (Ideal.Quotient.mk I) ⁻¹' ((Ideal.Quotient.mk I) '' s) = ⋃ (x : I), (fun (y : R) => x + y) '' s

      If I is an ideal of a commutative ring R, if q : R → R/I is the quotient map, and if s ⊆ R is a subset, then q⁻¹(q(s)) = ⋃ᵢ(i + s), the union running over all i ∈ I.

      instance Ideal.Quotient.noZeroDivisors {R : Type u} [CommRing R] (I : Ideal R) [hI : I.IsPrime] :
      Equations
      • =
      instance Ideal.Quotient.isDomain {R : Type u} [CommRing R] (I : Ideal R) [hI : I.IsPrime] :
      Equations
      • =
      theorem Ideal.Quotient.isDomain_iff_prime {R : Type u} [CommRing R] (I : Ideal R) :
      IsDomain (R I) I.IsPrime
      theorem Ideal.Quotient.exists_inv {R : Type u} [CommRing R] {I : Ideal R} [hI : I.IsMaximal] {a : R I} :
      a 0∃ (b : R I), a * b = 1
      @[reducible, inline]
      noncomputable abbrev Ideal.Quotient.groupWithZero {R : Type u} [CommRing R] (I : Ideal R) [hI : I.IsMaximal] :

      The quotient by a maximal ideal is a group with zero. This is a def rather than instance, since users will have computable inverses in some applications.

      See note [reducible non-instances].

      Equations
      Instances For
        @[reducible, inline]
        noncomputable abbrev Ideal.Quotient.field {R : Type u} [CommRing R] (I : Ideal R) [I.IsMaximal] :
        Field (R I)

        The quotient by a maximal ideal is a field. This is a def rather than instance, since users will have computable inverses (and qsmul, ratCast) in some applications.

        See note [reducible non-instances].

        Equations
        Instances For
          theorem Ideal.Quotient.maximal_of_isField {R : Type u} [CommRing R] (I : Ideal R) (hqf : IsField (R I)) :
          I.IsMaximal

          If the quotient by an ideal is a field, then the ideal is maximal.

          theorem Ideal.Quotient.maximal_ideal_iff_isField_quotient {R : Type u} [CommRing R] (I : Ideal R) :
          I.IsMaximal IsField (R I)

          The quotient of a ring by an ideal is a field iff the ideal is maximal.

          def Ideal.Quotient.lift {R : Type u} [CommRing R] {S : Type v} [Semiring S] (I : Ideal R) (f : R →+* S) (H : aI, f a = 0) :
          R I →+* S

          Given a ring homomorphism f : R →+* S sending all elements of an ideal to zero, lift it to the quotient by this ideal.

          Equations
          Instances For
            @[simp]
            theorem Ideal.Quotient.lift_mk {R : Type u} [CommRing R] {a : R} {S : Type v} [Semiring S] (I : Ideal R) (f : R →+* S) (H : aI, f a = 0) :
            theorem Ideal.Quotient.lift_surjective_of_surjective {R : Type u} [CommRing R] {S : Type v} [Semiring S] (I : Ideal R) {f : R →+* S} (H : aI, f a = 0) (hf : Function.Surjective f) :
            def Ideal.Quotient.factor {R : Type u} [CommRing R] (S : Ideal R) (T : Ideal R) (H : S T) :
            R S →+* R T

            The ring homomorphism from the quotient by a smaller ideal to the quotient by a larger ideal.

            This is the Ideal.Quotient version of Quot.Factor

            Equations
            Instances For
              @[simp]
              theorem Ideal.Quotient.factor_mk {R : Type u} [CommRing R] (S : Ideal R) (T : Ideal R) (H : S T) (x : R) :
              @[simp]
              theorem Ideal.Quotient.factor_comp_mk {R : Type u} [CommRing R] (S : Ideal R) (T : Ideal R) (H : S T) :
              def Ideal.quotEquivOfEq {R : Type u_1} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I = J) :
              R I ≃+* R J

              Quotienting by equal ideals gives equivalent rings.

              See also Submodule.quotEquivOfEq and Ideal.quotientEquivAlgOfEq.

              Equations
              Instances For
                @[simp]
                theorem Ideal.quotEquivOfEq_mk {R : Type u_1} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I = J) (x : R) :
                @[simp]
                theorem Ideal.quotEquivOfEq_symm {R : Type u_1} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I = J) :
                instance Ideal.modulePi {R : Type u} [CommRing R] (I : Ideal R) (ι : Type v) :
                Module (R I) ((ιR) I.pi ι)

                R^n/I^n is a R/I-module.

                Equations
                noncomputable def Ideal.piQuotEquiv {R : Type u} [CommRing R] (I : Ideal R) (ι : Type v) :
                ((ιR) I.pi ι) ≃ₗ[R I] ιR I

                R^n/I^n is isomorphic to (R/I)^n as an R/I-module.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem Ideal.map_pi {R : Type u} [CommRing R] (I : Ideal R) {ι : Type u_1} [Finite ι] {ι' : Type w} (x : ιR) (hi : ∀ (i : ι), x i I) (f : (ιR) →ₗ[R] ι'R) (i : ι') :
                  f x i I

                  If f : R^n → R^m is an R-linear map and I ⊆ R is an ideal, then the image of I^n is contained in I^m.

                  theorem Ideal.univ_eq_iUnion_image_add {R : Type u_1} [Ring R] (I : Ideal R) :
                  Set.univ = ⋃ (x : R I), Quotient.out' x +ᵥ I

                  A ring is made up of a disjoint union of cosets of an ideal.

                  theorem Finite.of_finite_quot_finite_ideal {R : Type u_1} [Ring R] {I : Ideal R} [hI : Finite I] [h : Finite (R I)] :