Documentation

Mathlib.RingTheory.Ideal.QuotientOperations

More operations on modules and ideals related to quotients #

Main results: #

def RingHom.kerLift {R : Type u} {S : Type v} [CommRing R] [Semiring S] (f : R →+* S) :

The induced map from the quotient by the kernel to the codomain.

This is an isomorphism if f has a right inverse (quotientKerEquivOfRightInverse) / is surjective (quotientKerEquivOfSurjective).

Equations
Instances For
    @[simp]
    theorem RingHom.kerLift_mk {R : Type u} {S : Type v} [CommRing R] [Semiring S] (f : R →+* S) (r : R) :
    theorem RingHom.lift_injective_of_ker_le_ideal {R : Type u} {S : Type v} [CommRing R] [Semiring S] (I : Ideal R) {f : R →+* S} (H : aI, f a = 0) (hI : RingHom.ker f I) :

    The induced map from the quotient by the kernel is injective.

    def RingHom.quotientKerEquivOfRightInverse {R : Type u} {S : Type v} [CommRing R] [Semiring S] {f : R →+* S} {g : SR} (hf : Function.RightInverse g f) :

    The first isomorphism theorem for commutative rings, computable version.

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

      The quotient of a ring by he zero ideal is isomorphic to the ring itself.

      Equations
      Instances For
        noncomputable def RingHom.quotientKerEquivOfSurjective {R : Type u} {S : Type v} [CommRing R] [Semiring S] {f : R →+* S} (hf : Function.Surjective f) :

        The first isomorphism theorem for commutative rings, surjective case.

        Equations
        Instances For
          noncomputable def RingHom.quotientKerEquivRangeS {R : Type u} {S : Type v} [CommRing R] [Semiring S] (f : R →+* S) :

          The first isomorphism theorem for commutative rings (RingHom.rangeS version).

          Equations
          Instances For
            noncomputable def RingHom.quotientKerEquivRange {R : Type u} [CommRing R] {S : Type v} [Ring S] (f : R →+* S) :

            The first isomorphism theorem for commutative rings (RingHom.range version).

            Equations
            Instances For
              @[simp]
              theorem Ideal.mk_ker {R : Type u} [CommRing R] {I : Ideal R} :
              theorem Ideal.map_mk_eq_bot_of_le {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I J) :
              theorem Ideal.injective_lift_iff {R : Type u} {S : Type v} [CommRing R] [Semiring S] {I : Ideal R} {f : R →+* S} (H : aI, f a = 0) :
              theorem Ideal.ker_Pi_Quotient_mk {R : Type u} [CommRing R] {ι : Type u_1} (I : ιIdeal R) :
              RingHom.ker (Pi.ringHom fun (i : ι) => Ideal.Quotient.mk (I i)) = ⨅ (i : ι), I i
              @[simp]
              theorem Ideal.mem_quotient_iff_mem_sup {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} {x : R} :

              See also Ideal.mem_quotient_iff_mem in case I ≤ J.

              theorem Ideal.mem_quotient_iff_mem {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (hIJ : I J) {x : R} :

              See also Ideal.mem_quotient_iff_mem_sup if the assumption I ≤ J is not available.

              def Ideal.quotientInfToPiQuotient {R : Type u} [CommRing R] {ι : Type u_1} (I : ιIdeal R) :
              R ⨅ (i : ι), I i →+* (i : ι) → R I i

              The homomorphism from R/(⋂ i, f i) to ∏ i, (R / f i) featured in the Chinese Remainder Theorem. It is bijective if the ideals f i are coprime.

              Equations
              Instances For
                theorem Ideal.quotientInfToPiQuotient_mk {R : Type u} [CommRing R] {ι : Type u_1} (I : ιIdeal R) (x : R) :
                (Ideal.quotientInfToPiQuotient I) ((Ideal.Quotient.mk (⨅ (i : ι), I i)) x) = fun (i : ι) => (Ideal.Quotient.mk (I i)) x
                theorem Ideal.quotientInfToPiQuotient_mk' {R : Type u} [CommRing R] {ι : Type u_1} (I : ιIdeal R) (x : R) (i : ι) :
                (Ideal.quotientInfToPiQuotient I) ((Ideal.Quotient.mk (⨅ (i : ι), I i)) x) i = (Ideal.Quotient.mk (I i)) x
                theorem Ideal.quotientInfToPiQuotient_surj {R : Type u} [CommRing R] {ι : Type u_1} [Finite ι] {I : ιIdeal R} (hI : Pairwise fun (i j : ι) => IsCoprime (I i) (I j)) :
                noncomputable def Ideal.quotientInfRingEquivPiQuotient {R : Type u} [CommRing R] {ι : Type u_1} [Finite ι] (f : ιIdeal R) (hf : Pairwise fun (i j : ι) => IsCoprime (f i) (f j)) :
                R ⨅ (i : ι), f i ≃+* ((i : ι) → R f i)

                Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  noncomputable def Ideal.quotientInfEquivQuotientProd {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : IsCoprime I J) :
                  R I J ≃+* (R I) × R J

                  Chinese remainder theorem, specialized to two ideals.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem Ideal.quotientInfEquivQuotientProd_fst {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : IsCoprime I J) (x : R I J) :
                    @[simp]
                    theorem Ideal.quotientInfEquivQuotientProd_snd {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : IsCoprime I J) (x : R I J) :
                    @[simp]
                    theorem Ideal.fst_comp_quotientInfEquivQuotientProd {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : IsCoprime I J) :
                    @[simp]
                    theorem Ideal.snd_comp_quotientInfEquivQuotientProd {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : IsCoprime I J) :
                    instance Ideal.Quotient.algebra (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I : Ideal A} :
                    Algebra R₁ (A I)

                    The R₁-algebra structure on A/I for an R₁-algebra A

                    Equations
                    instance Ideal.Quotient.isScalarTower (R₁ : Type u_1) (R₂ : Type u_2) {A : Type u_3} [CommSemiring R₁] [CommSemiring R₂] [CommRing A] [Algebra R₁ A] [Algebra R₂ A] [SMul R₁ R₂] [IsScalarTower R₁ R₂ A] (I : Ideal A) :
                    IsScalarTower R₁ R₂ (A I)
                    Equations
                    • =
                    def Ideal.Quotient.mkₐ (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) :
                    A →ₐ[R₁] A I

                    The canonical morphism A →ₐ[R₁] A ⧸ I as morphism of R₁-algebras, for I an ideal of A, where A is an R₁-algebra.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem Ideal.Quotient.algHom_ext (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I : Ideal A} {S : Type u_5} [Semiring S] [Algebra R₁ S] ⦃f : A I →ₐ[R₁] S ⦃g : A I →ₐ[R₁] S (h : AlgHom.comp f (Ideal.Quotient.mkₐ R₁ I) = AlgHom.comp g (Ideal.Quotient.mkₐ R₁ I)) :
                      f = g
                      theorem Ideal.Quotient.alg_map_eq (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) :
                      algebraMap R₁ (A I) = RingHom.comp (algebraMap A (A I)) (algebraMap R₁ A)
                      theorem Ideal.Quotient.mkₐ_toRingHom (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) :
                      @[simp]
                      theorem Ideal.Quotient.mkₐ_eq_mk (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) :
                      @[simp]
                      theorem Ideal.Quotient.mk_comp_algebraMap (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) :
                      @[simp]
                      theorem Ideal.Quotient.mk_algebraMap (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) (x : R₁) :
                      (Ideal.Quotient.mk I) ((algebraMap R₁ A) x) = (algebraMap R₁ (A I)) x
                      theorem Ideal.Quotient.mkₐ_surjective (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) :

                      The canonical morphism A →ₐ[R₁] I.quotient is surjective.

                      @[simp]
                      theorem Ideal.Quotient.mkₐ_ker (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) :

                      The kernel of A →ₐ[R₁] I.quotient is I.

                      def Ideal.Quotient.liftₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (I : Ideal A) (f : A →ₐ[R₁] B) (hI : aI, f a = 0) :
                      A I →ₐ[R₁] B

                      Ideal.quotient.lift as an AlgHom.

                      Equations
                      Instances For
                        @[simp]
                        theorem Ideal.Quotient.liftₐ_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (I : Ideal A) (f : A →ₐ[R₁] B) (hI : aI, f a = 0) (x : A I) :
                        (Ideal.Quotient.liftₐ I f hI) x = (Ideal.Quotient.lift I (f) hI) x
                        theorem Ideal.Quotient.liftₐ_comp {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (I : Ideal A) (f : A →ₐ[R₁] B) (hI : aI, f a = 0) :
                        theorem Ideal.KerLift.map_smul {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) (r : R₁) (x : A RingHom.ker f) :
                        (RingHom.kerLift f.toRingHom) (r x) = r (RingHom.kerLift f.toRingHom) x
                        def Ideal.kerLiftAlg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) :

                        The induced algebras morphism from the quotient by the kernel to the codomain.

                        This is an isomorphism if f has a right inverse (quotientKerAlgEquivOfRightInverse) / is surjective (quotientKerAlgEquivOfSurjective).

                        Equations
                        Instances For
                          @[simp]
                          theorem Ideal.kerLiftAlg_mk {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) (a : A) :
                          @[simp]
                          theorem Ideal.kerLiftAlg_toRingHom {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) :
                          theorem Ideal.kerLiftAlg_injective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) :

                          The induced algebra morphism from the quotient by the kernel is injective.

                          @[simp]
                          theorem Ideal.quotientKerAlgEquivOfRightInverse_symm_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : Function.RightInverse g f) :
                          @[simp]
                          theorem Ideal.quotientKerAlgEquivOfRightInverse_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : Function.RightInverse g f) (a : A RingHom.ker f.toRingHom) :
                          def Ideal.quotientKerAlgEquivOfRightInverse {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : Function.RightInverse g f) :

                          The first isomorphism theorem for algebras, computable version.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[deprecated Ideal.quotientKerAlgEquivOfRightInverse_apply]
                            theorem Ideal.quotientKerAlgEquivOfRightInverse.apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : Function.RightInverse g f) (a : A RingHom.ker f.toRingHom) :

                            Alias of Ideal.quotientKerAlgEquivOfRightInverse_apply.

                            @[deprecated Ideal.quotientKerAlgEquivOfRightInverse_symm_apply]
                            theorem Ideal.QuotientKerAlgEquivOfRightInverseSymm.apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : Function.RightInverse g f) :

                            Alias of Ideal.quotientKerAlgEquivOfRightInverse_symm_apply.

                            @[simp]
                            theorem Ideal.quotientKerAlgEquivOfSurjective_symm_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective f) :
                            @[simp]
                            theorem Ideal.quotientKerAlgEquivOfSurjective_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective f) (a : A RingHom.ker f.toRingHom) :
                            noncomputable def Ideal.quotientKerAlgEquivOfSurjective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective f) :

                            The first isomorphism theorem for algebras.

                            Equations
                            Instances For
                              def Ideal.quotientMap {R : Type u} [CommRing R] {S : Type v} [CommRing S] {I : Ideal R} (J : Ideal S) (f : R →+* S) (hIJ : I Ideal.comap f J) :
                              R I →+* S J

                              The ring hom R/I →+* S/J induced by a ring hom f : R →+* S with I ≤ f⁻¹(J)

                              Equations
                              Instances For
                                @[simp]
                                theorem Ideal.quotientMap_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} {H : J Ideal.comap f I} {x : R} :
                                @[simp]
                                theorem Ideal.quotientMap_algebraMap {R₁ : Type u_1} {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {S : Type v} [CommRing S] {J : Ideal A} {I : Ideal S} {f : A →+* S} {H : J Ideal.comap f I} {x : R₁} :
                                (Ideal.quotientMap I f H) ((algebraMap R₁ (A J)) x) = (Ideal.Quotient.mk I) (f ((algebraMap R₁ A) x))
                                @[simp]
                                theorem Ideal.quotientEquiv_symm_apply {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (f) I) (a : S J) :
                                @[simp]
                                theorem Ideal.quotientEquiv_apply {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (f) I) :
                                ∀ (a : R I), (Ideal.quotientEquiv I J f hIJ) a = (Ideal.quotientMap J f ).toFun a
                                def Ideal.quotientEquiv {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (f) I) :
                                R I ≃+* S J

                                The ring equiv R/I ≃+* S/J induced by a ring equiv f : R ≃+** S, where J = f(I).

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem Ideal.quotientEquiv_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (f) I) (x : R) :
                                  @[simp]
                                  theorem Ideal.quotientEquiv_symm_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (f) I) (x : S) :
                                  theorem Ideal.quotientMap_injective' {R : Type u} [CommRing R] {S : Type v} [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} {H : J Ideal.comap f I} (h : Ideal.comap f I J) :

                                  H and h are kept as separate hypothesis since H is used in constructing the quotient map.

                                  theorem Ideal.quotientMap_injective {R : Type u} [CommRing R] {S : Type v} [CommRing S] {I : Ideal S} {f : R →+* S} :

                                  If we take J = I.comap f then QuotientMap is injective automatically.

                                  theorem Ideal.quotientMap_surjective {R : Type u} [CommRing R] {S : Type v} [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} {H : J Ideal.comap f I} (hf : Function.Surjective f) :
                                  theorem Ideal.comp_quotientMap_eq_of_comp_eq {R : Type u} [CommRing R] {S : Type v} [CommRing S] {R' : Type u_5} {S' : Type u_6} [CommRing R'] [CommRing S'] {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : RingHom.comp f' g = RingHom.comp g' f) (I : Ideal S') :

                                  Commutativity of a square is preserved when taking quotients by an ideal.

                                  def Ideal.quotientMapₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [CommRing B] [Algebra R₁ B] {I : Ideal A} (J : Ideal B) (f : A →ₐ[R₁] B) (hIJ : I Ideal.comap f J) :
                                  A I →ₐ[R₁] B J

                                  The algebra hom A/I →+* B/J induced by an algebra hom f : A →ₐ[R₁] B with I ≤ f⁻¹(J).

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Ideal.quotient_map_mkₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [CommRing B] [Algebra R₁ B] {I : Ideal A} (J : Ideal B) (f : A →ₐ[R₁] B) (H : I Ideal.comap f J) {x : A} :
                                    theorem Ideal.quotient_map_comp_mkₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [CommRing B] [Algebra R₁ B] {I : Ideal A} (J : Ideal B) (f : A →ₐ[R₁] B) (H : I Ideal.comap f J) :
                                    def Ideal.quotientEquivAlg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [CommRing B] [Algebra R₁ B] (I : Ideal A) (J : Ideal B) (f : A ≃ₐ[R₁] B) (hIJ : J = Ideal.map (f) I) :
                                    (A I) ≃ₐ[R₁] B J

                                    The algebra equiv A/I ≃ₐ[R] B/J induced by an algebra equiv f : A ≃ₐ[R] B, whereJ = f(I).

                                    Equations
                                    Instances For
                                      instance Ideal.quotientAlgebra {R : Type u} [CommRing R] {A : Type u_3} [CommRing A] {I : Ideal A} [Algebra R A] :
                                      Equations
                                      def Ideal.quotientEquivAlgOfEq (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I : Ideal A} {J : Ideal A} (h : I = J) :
                                      (A I) ≃ₐ[R₁] A J

                                      Quotienting by equal ideals gives equivalent algebras.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Ideal.quotientEquivAlgOfEq_mk (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I : Ideal A} {J : Ideal A} (h : I = J) (x : A) :
                                        @[simp]
                                        theorem Ideal.quotientEquivAlgOfEq_symm (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I : Ideal A} {J : Ideal A} (h : I = J) :
                                        theorem Ideal.comap_map_mk {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I J) :
                                        noncomputable def Ideal.quotientKerEquivRange {R : Type u} [CommRing R] {A : Type u_5} {B : Type u_6} [CommRing A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :

                                        The first isomorphism theorem for commutative algebras (AlgHom.range version).

                                        Equations
                                        Instances For
                                          def DoubleQuot.quotLeftToQuotSup {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) :
                                          R I →+* R I J

                                          The obvious ring hom R/I → R/(I ⊔ J)

                                          Equations
                                          Instances For
                                            def DoubleQuot.quotQuotToQuotSup {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) :

                                            The ring homomorphism (R/I)/J' -> R/(I ⊔ J) induced by quotLeftToQuotSup where J' is the image of J in R/I

                                            Equations
                                            Instances For
                                              def DoubleQuot.quotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) :

                                              The composite of the maps R → (R/I) and (R/I) → (R/I)/J'

                                              Equations
                                              Instances For

                                                The kernel of quotQuotMk

                                                def DoubleQuot.liftSupQuotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) :

                                                The ring homomorphism R/(I ⊔ J) → (R/I)/J' induced by quotQuotMk

                                                Equations
                                                Instances For

                                                  quotQuotToQuotSup and liftSupQuotQuotMk are inverse isomorphisms. In the case where I ≤ J, this is the Third Isomorphism Theorem (see quotQuotEquivQuotOfLe)

                                                  Equations
                                                  Instances For
                                                    def DoubleQuot.quotQuotEquivQuotOfLE {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I J) :

                                                    The Third Isomorphism theorem for rings. See quotQuotEquivQuotSup for a version that does not assume an inclusion of ideals.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      @[simp]
                                                      def DoubleQuot.quotLeftToQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) :
                                                      A I →ₐ[R] A I J

                                                      The natural algebra homomorphism A / I → A / (I ⊔ J).

                                                      Equations
                                                      Instances For
                                                        def DoubleQuot.quotQuotToQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) :

                                                        The algebra homomorphism (A / I) / J' -> A / (I ⊔ J) induced by quotQuotToQuotSup, where J' is the projection of J in A / I.

                                                        Equations
                                                        Instances For
                                                          def DoubleQuot.quotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) :

                                                          The composition of the algebra homomorphisms A → (A / I) and (A / I) → (A / I) / J', where J' is the projection J in A / I.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            @[simp]
                                                            theorem DoubleQuot.coe_quotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) :
                                                            def DoubleQuot.liftSupQuotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) :

                                                            The injective algebra homomorphism A / (I ⊔ J) → (A / I) / J'induced by quot_quot_mk, where J' is the projection J in A / I.

                                                            Equations
                                                            Instances For
                                                              def DoubleQuot.quotQuotEquivQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) :

                                                              quotQuotToQuotSup and liftSupQuotQuotMk are inverse isomorphisms. In the case where I ≤ J, this is the Third Isomorphism Theorem (see DoubleQuot.quotQuotEquivQuotOfLE).

                                                              Equations
                                                              Instances For

                                                                The natural algebra isomorphism (A / I) / J' → (A / J) / I', where J' (resp. I') is the projection of J in A / I (resp. I in A / J).

                                                                Equations
                                                                Instances For
                                                                  def DoubleQuot.quotQuotEquivQuotOfLEₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I : Ideal A} {J : Ideal A} (h : I J) :

                                                                  The third isomorphism theorem for algebras. See quotQuotEquivQuotSupₐ for version that does not assume an inclusion of ideals.

                                                                  Equations
                                                                  Instances For