Documentation

Mathlib.RingTheory.Ideal.Quotient.Defs

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 #

instance Ideal.instHasQuotient {R : Type u} [Ring R] :

The quotient R/I of a ring R by an ideal I, defined to equal the quotient of I as an R-submodule of R.

Equations
    instance Ideal.instHasQuotient_1 {R : Type u_1} [CommRing R] :

    Shortcut instance for commutative rings.

    Equations
      instance Ideal.Quotient.one {R : Type u} [Ring R] (I : Ideal R) :
      One (R I)
      Equations
        def Ideal.Quotient.ringCon {R : Type u} [Ring R] (I : Ideal R) [I.IsTwoSided] :

        On Ideals, Submodule.quotientRel is a ring congruence.

        Equations
          Instances For
            instance Ideal.Quotient.ring {R : Type u} [Ring R] (I : Ideal R) [I.IsTwoSided] :
            Ring (R I)
            Equations
              instance Ideal.Quotient.commRing {R : Type u_1} [CommRing R] (I : Ideal R) :
              Equations
                instance Ideal.Quotient.instRingQuotient {R : Type u_1} [CommRing R] (I : Ideal R) :
                Ring (R I)
                Equations
                  instance Ideal.Quotient.commSemiring {R : Type u_1} [CommRing R] (I : Ideal R) :
                  Equations
                    instance Ideal.Quotient.semiring {R : Type u_1} [CommRing R] (I : Ideal R) :
                    Equations
                      def Ideal.Quotient.mk {R : Type u} [Ring R] (I : Ideal R) [I.IsTwoSided] :
                      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} [Ring R] {I : Ideal R} [I.IsTwoSided] :
                          Coe R (R I)
                          Equations
                            theorem Ideal.Quotient.ringHom_ext {R : Type u} [Ring R] {I : Ideal R} {S : Type v} [I.IsTwoSided] [NonAssocSemiring S] f g : R I →+* S (h : f.comp (mk I) = g.comp (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].

                            theorem Ideal.Quotient.ringHom_ext_iff {R : Type u} [Ring R] {I : Ideal R} {S : Type v} [I.IsTwoSided] [NonAssocSemiring S] {f g : R I →+* S} :
                            f = g f.comp (mk I) = g.comp (mk I)
                            theorem Ideal.Quotient.eq {R : Type u} [Ring R] {I : Ideal R} {x y : R} [I.IsTwoSided] :
                            (mk I) x = (mk I) y x - y I
                            @[simp]
                            theorem Ideal.Quotient.mk_eq_mk {R : Type u} [Ring R] {I : Ideal R} [I.IsTwoSided] (x : R) :
                            theorem Ideal.Quotient.eq_zero_iff_mem {R : Type u} [Ring R] {I : Ideal R} {a : R} [I.IsTwoSided] :
                            (mk I) a = 0 a I
                            theorem Ideal.Quotient.mk_eq_mk_iff_sub_mem {R : Type u} [Ring R] {I : Ideal R} [I.IsTwoSided] (x y : R) :
                            (mk I) x = (mk I) y x - y I
                            @[simp]
                            theorem Ideal.Quotient.mk_out {R : Type u} [Ring R] {I : Ideal R} [I.IsTwoSided] (x : R I) :
                            (mk I) (Quotient.out x) = x
                            theorem Ideal.Quotient.quotient_ring_saturate {R : Type u} [Ring R] {I : Ideal R} [I.IsTwoSided] (s : Set R) :
                            (mk I) ⁻¹' ((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.

                            def Ideal.Quotient.lift {R : Type u} [Ring R] (I : Ideal R) {S : Type v} [I.IsTwoSided] [Semiring S] (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} [Ring R] (I : Ideal R) {a : R} {S : Type v} [I.IsTwoSided] [Semiring S] (f : R →+* S) (H : aI, f a = 0) :
                                (lift I f H) ((mk I) a) = f a
                                theorem Ideal.Quotient.lift_comp_mk {R : Type u} [Ring R] (I : Ideal R) {S : Type v} [I.IsTwoSided] [Semiring S] (f : R →+* S) (H : aI, f a = 0) :
                                (lift I f H).comp (mk I) = f
                                theorem Ideal.Quotient.lift_surjective_of_surjective {R : Type u} [Ring R] (I : Ideal R) {S : Type v} [I.IsTwoSided] [Semiring S] {f : R →+* S} (H : aI, f a = 0) (hf : Function.Surjective f) :
                                def Ideal.Quotient.factor {R : Type u} [Ring R] {S T : Ideal R} [S.IsTwoSided] [T.IsTwoSided] (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

                                When the two ideals are of the form I^m and I^n and n ≤ m, please refer to the dedicated version Ideal.Quotient.factorPow.

                                Equations
                                  Instances For
                                    @[simp]
                                    theorem Ideal.Quotient.factor_mk {R : Type u} [Ring R] {S T : Ideal R} [S.IsTwoSided] [T.IsTwoSided] (H : S T) (x : R) :
                                    (factor H) ((mk S) x) = (mk T) x
                                    @[simp]
                                    theorem Ideal.Quotient.factor_eq {R : Type u} [Ring R] {S : Ideal R} [S.IsTwoSided] :
                                    @[simp]
                                    theorem Ideal.Quotient.factor_comp_mk {R : Type u} [Ring R] {S T : Ideal R} [S.IsTwoSided] [T.IsTwoSided] (H : S T) :
                                    (factor H).comp (mk S) = mk T
                                    @[simp]
                                    theorem Ideal.Quotient.factor_comp {R : Type u} [Ring R] {S T U : Ideal R} [S.IsTwoSided] [T.IsTwoSided] [U.IsTwoSided] (H1 : S T) (H2 : T U) :
                                    (factor H2).comp (factor H1) = factor
                                    @[simp]
                                    theorem Ideal.Quotient.factor_comp_apply {R : Type u} [Ring R] {S T U : Ideal R} [S.IsTwoSided] [T.IsTwoSided] [U.IsTwoSided] (H1 : S T) (H2 : T U) (x : R S) :
                                    (factor H2) ((factor H1) x) = (factor ) x
                                    def Ideal.quotEquivOfEq {R : Type u} [Ring R] {I J : Ideal R} [I.IsTwoSided] [J.IsTwoSided] (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} [Ring R] {I J : Ideal R} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) (x : R) :
                                        @[simp]
                                        theorem Ideal.quotEquivOfEq_symm {R : Type u} [Ring R] {I J : Ideal R} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) :