# mathlib3documentation

ring_theory.ideal.quotient_operations

# More operations on modules and ideals related to quotients #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

def ring_hom.ker_lift {R : Type u} {S : Type v} [comm_ring R] [comm_ring 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 (`quotient_ker_equiv_of_right_inverse`) / is surjective (`quotient_ker_equiv_of_surjective`).

Equations
@[simp]
theorem ring_hom.ker_lift_mk {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (r : R) :
(f.ker_lift) ( r) = f r
theorem ring_hom.ker_lift_injective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

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

theorem ring_hom.lift_injective_of_ker_le_ideal {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (I : ideal R) {f : R →+* S} (H : (a : R), a I f a = 0) (hI : I) :
def ring_hom.quotient_ker_equiv_of_right_inverse {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {g : S R} (hf : f) :

The first isomorphism theorem for commutative rings, computable version.

Equations
@[simp]
theorem ring_hom.quotient_ker_equiv_of_right_inverse.apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {g : S R} (hf : f) (x : R ) :
@[simp]
theorem ring_hom.quotient_ker_equiv_of_right_inverse.symm.apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {g : S R} (hf : f) (x : S) :
= (g x)
noncomputable def ring_hom.quotient_ker_equiv_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective f) :

The first isomorphism theorem for commutative rings.

Equations
@[simp]
theorem ideal.map_quotient_self {R : Type u} [comm_ring R] (I : ideal R) :
@[simp]
theorem ideal.mk_ker {R : Type u} [comm_ring R] {I : ideal R} :
theorem ideal.map_mk_eq_bot_of_le {R : Type u} [comm_ring R] {I J : ideal R} (h : I J) :
theorem ideal.ker_quotient_lift {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {I : ideal R} (f : R →+* S) (H : I ) :
@[simp]
theorem ideal.bot_quotient_is_maximal_iff {R : Type u} [comm_ring R] (I : ideal R) :
@[simp]
theorem ideal.mem_quotient_iff_mem_sup {R : Type u} [comm_ring R] {I J : ideal R} {x : R} :
x x J I

See also `ideal.mem_quotient_iff_mem` in case `I ≤ J`.

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

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

theorem ideal.comap_map_mk {R : Type u} [comm_ring R] {I J : ideal R} (h : I J) :
J) = J
@[protected, instance]
def ideal.quotient.algebra (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] {I : ideal A} :
algebra R₁ (A I)

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

Equations
@[protected, instance]
def ideal.quotient.is_scalar_tower (R₁ : Type u_1) (R₂ : Type u_2) {A : Type u_3} [comm_semiring R₁] [comm_semiring R₂] [comm_ring A] [algebra R₁ A] [algebra R₂ A] [has_smul R₁ R₂] [ R₂ A] (I : ideal A) :
R₂ (A I)
def ideal.quotient.mkₐ (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring 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
theorem ideal.quotient.alg_hom_ext (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] {I : ideal A} {S : Type u_2} [semiring S] [algebra R₁ S] ⦃f g : A I →ₐ[R₁] S⦄ (h : f.comp I) = g.comp I)) :
f = g
theorem ideal.quotient.alg_map_eq (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
(A I) = (A I)).comp (algebra_map R₁ A)
theorem ideal.quotient.mkₐ_to_ring_hom (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
@[simp]
theorem ideal.quotient.mkₐ_eq_mk (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
I) =
@[simp]
theorem ideal.quotient.algebra_map_eq {R : Type u} [comm_ring R] (I : ideal R) :
(R I) =
@[simp]
theorem ideal.quotient.mk_comp_algebra_map (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
(algebra_map R₁ A) = (A I)
@[simp]
theorem ideal.quotient.mk_algebra_map (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) (x : R₁) :
((algebra_map R₁ A) x) = (algebra_map R₁ (A I)) x
theorem ideal.quotient.mkₐ_surjective (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring 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} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
= I

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} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (I : ideal A) (f : A →ₐ[R₁] B) (hI : (a : A), a I f a = 0) :
A I →ₐ[R₁] B

`ideal.quotient.lift` as an `alg_hom`.

Equations
@[simp]
theorem ideal.quotient.liftₐ_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (I : ideal A) (f : A →ₐ[R₁] B) (hI : (a : A), a I f a = 0) (x : A I) :
hI) x = hI) x
theorem ideal.quotient.liftₐ_comp {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (I : ideal A) (f : A →ₐ[R₁] B) (hI : (a : A), a I f a = 0) :
hI).comp I) = f
theorem ideal.ker_lift.map_smul {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) (r : R₁) (x : A ) :
def ideal.ker_lift_alg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) :
→ₐ[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 (`quotient_ker_alg_equiv_of_right_inverse`) / is surjective (`quotient_ker_alg_equiv_of_surjective`).

Equations
@[simp]
theorem ideal.ker_lift_alg_mk {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) (a : A) :
a) = f a
@[simp]
theorem ideal.ker_lift_alg_to_ring_hom {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) :
theorem ideal.ker_lift_alg_injective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) :

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

def ideal.quotient_ker_alg_equiv_of_right_inverse {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {f : A →ₐ[R₁] B} {g : B A} (hf : f) :
(A ≃ₐ[R₁] B

The first isomorphism theorem for algebras, computable version.

Equations
@[simp]
theorem ideal.quotient_ker_alg_equiv_of_right_inverse.apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {f : A →ₐ[R₁] B} {g : B A} (hf : f) (x : A ) :
@[simp]
theorem ideal.quotient_ker_alg_equiv_of_right_inverse_symm.apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {f : A →ₐ[R₁] B} {g : B A} (hf : f) (x : B) :
= (g x)
noncomputable def ideal.quotient_ker_alg_equiv_of_surjective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {f : A →ₐ[R₁] B} (hf : function.surjective f) :
(A ≃ₐ[R₁] B

The first isomorphism theorem for algebras.

Equations
def ideal.quotient_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {I : ideal R} (J : ideal S) (f : R →+* S) (hIJ : I 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
@[simp]
theorem ideal.quotient_map_mk {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} {H : J I} {x : R} :
(I.quotient_map f H) ( x) = (f x)
@[simp]
theorem ideal.quotient_map_algebra_map {S : Type v} [comm_ring S] {R₁ : Type u_1} {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] {J : ideal A} {I : ideal S} {f : A →+* S} {H : J I} {x : R₁} :
(I.quotient_map f H) ((algebra_map R₁ (A J)) x) = (f ((algebra_map R₁ A) x))
theorem ideal.quotient_map_comp_mk {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} (H : J I) :
(I.quotient_map f H).comp = f
@[simp]
theorem ideal.quotient_equiv_symm_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = I) (ᾰ : S J) :
((I.quotient_equiv J f hIJ).symm) = (I.quotient_map (f.symm) _)
def ideal.quotient_equiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = 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
@[simp]
theorem ideal.quotient_equiv_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = I) (ᾰ : R I) :
(I.quotient_equiv J f hIJ) = (J.quotient_map f _).to_fun
@[simp]
theorem ideal.quotient_equiv_mk {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = I) (x : R) :
(I.quotient_equiv J f hIJ) ( x) = (f x)
@[simp]
theorem ideal.quotient_equiv_symm_mk {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = I) (x : S) :
((I.quotient_equiv J f hIJ).symm) ( x) = ((f.symm) x)
theorem ideal.quotient_map_injective' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} {H : J I} (h : I J) :

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

theorem ideal.quotient_map_injective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {I : ideal S} {f : R →+* S} :

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

theorem ideal.quotient_map_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} {H : J I} (hf : function.surjective f) :
theorem ideal.comp_quotient_map_eq_of_comp_eq {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {R' : Type u_1} {S' : Type u_2} [comm_ring R'] [comm_ring S'] {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : f'.comp g = g'.comp f) (I : ideal S') :

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

def ideal.quotient_mapₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {I : ideal A} (J : ideal B) (f : A →ₐ[R₁] B) (hIJ : I 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
@[simp]
theorem ideal.quotient_map_mkₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {I : ideal A} (J : ideal B) (f : A →ₐ[R₁] B) (H : I J) {x : A} :
(J.quotient_mapₐ f H) ( x) = J) (f x)
theorem ideal.quotient_map_comp_mkₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {I : ideal A} (J : ideal B) (f : A →ₐ[R₁] B) (H : I J) :
(J.quotient_mapₐ f H).comp I) = J).comp f
def ideal.quotient_equiv_alg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (I : ideal A) (J : ideal B) (f : A ≃ₐ[R₁] B) (hIJ : J = I) :
(A I) ≃ₐ[R₁] B J

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

Equations
@[protected, instance]
def ideal.quotient_algebra {R : Type u} [comm_ring R] {A : Type u_3} [comm_ring A] {I : ideal A} [ A] :
algebra (R ideal.comap A) I) (A I)
Equations
def ideal.quotient_equiv_alg_of_eq (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] {I J : ideal A} (h : I = J) :
(A I) ≃ₐ[R₁] A J

Quotienting by equal ideals gives equivalent algebras.

Equations
@[simp]
theorem ideal.quotient_equiv_alg_of_eq_mk (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] {I J : ideal A} (h : I = J) (x : A) :
( x) = x
@[simp]
theorem ideal.quotient_equiv_alg_of_eq_symm (R₁ : Type u_1) {A : Type u_3} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] {I J : ideal A} (h : I = J) :
def double_quot.quot_left_to_quot_sup {R : Type u} [comm_ring R] (I J : ideal R) :
R I →+* R I J

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

Equations
theorem double_quot.ker_quot_left_to_quot_sup {R : Type u} [comm_ring R] (I J : ideal R) :

The kernel of `quot_left_to_quot_sup`

def double_quot.quot_quot_to_quot_sup {R : Type u} [comm_ring R] (I J : ideal R) :
(R I) →+* R I J

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

Equations
def double_quot.quot_quot_mk {R : Type u} [comm_ring R] (I J : ideal R) :
R →+* (R I)

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

Equations
theorem double_quot.ker_quot_quot_mk {R : Type u} [comm_ring R] (I J : ideal R) :
= I J

The kernel of `quot_quot_mk`

def double_quot.lift_sup_quot_quot_mk {R : Type u} [comm_ring R] (I J : ideal R) :
R I J →+* (R I)

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

Equations
def double_quot.quot_quot_equiv_quot_sup {R : Type u} [comm_ring R] (I J : ideal R) :
(R I) ≃+* R I J

`quot_quot_to_quot_add` and `lift_sup_double_qot_mk` are inverse isomorphisms. In the case where `I ≤ J`, this is the Third Isomorphism Theorem (see `quot_quot_equiv_quot_of_le`)

Equations
@[simp]
theorem double_quot.quot_quot_equiv_quot_sup_quot_quot_mk {R : Type u} [comm_ring R] (I J : ideal R) (x : R) :
( x) = (ideal.quotient.mk (I J)) x
@[simp]
def double_quot.quot_quot_equiv_comm {R : Type u} [comm_ring R] (I J : ideal R) :
(R I) ≃+* (R J)

The obvious isomorphism `(R/I)/J' → (R/J)/I'`

Equations
@[simp]
theorem double_quot.quot_quot_equiv_comm_quot_quot_mk {R : Type u} [comm_ring R] (I J : ideal R) (x : R) :
( x) = x
@[simp]
theorem double_quot.quot_quot_equiv_comm_symm {R : Type u} [comm_ring R] (I J : ideal R) :
def double_quot.quot_quot_equiv_quot_of_le {R : Type u} [comm_ring R] {I J : ideal R} (h : I J) :
(R I) ≃+* R J

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

Equations
@[simp]
theorem double_quot.quot_quot_equiv_quot_of_le_quot_quot_mk {R : Type u} [comm_ring R] {I J : ideal R} (x : R) (h : I J) :
= x
@[simp]
theorem double_quot.quot_quot_equiv_quot_of_le_symm_mk {R : Type u} [comm_ring R] {I J : ideal R} (x : R) (h : I J) :
= x
@[simp]
theorem double_quot.quot_quot_equiv_comm_mk_mk {R : Type u} [comm_ring R] (I J : ideal R) (x : R) :
((ideal.quotient.mk J)) ( x)) = ((R J) I)) x
@[simp]
theorem double_quot.quot_quot_equiv_quot_sup_quot_quot_algebra_map {R : Type u} {A : Type v} [comm_ring A] [ A] (I J : ideal A) (x : R) :
( ((A I) J)) x) = (A I J)) x
@[simp]
theorem double_quot.quot_quot_equiv_comm_algebra_map {R : Type u} {A : Type v} [comm_ring A] [ A] (I J : ideal A) (x : R) :
( ((A I) J)) x) = ((A J) I)) x
def double_quot.quot_left_to_quot_supₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
A I →ₐ[R] A I J

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

Equations
@[simp]
theorem double_quot.quot_left_to_quot_supₐ_to_ring_hom (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.coe_quot_left_to_quot_supₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
def double_quot.quot_quot_to_quot_supₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
(A I) J →ₐ[R] A I J

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

Equations
@[simp]
theorem double_quot.quot_quot_to_quot_supₐ_to_ring_hom (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.coe_quot_quot_to_quot_supₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
def double_quot.quot_quot_mkₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
A →ₐ[R] (A I) J

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
@[simp]
theorem double_quot.quot_quot_mkₐ_to_ring_hom (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.coe_quot_quot_mkₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
J) =
def double_quot.lift_sup_quot_quot_mkₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
A I J →ₐ[R] (A I) J

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
@[simp]
theorem double_quot.lift_sup_quot_quot_mkₐ_to_ring_hom (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.coe_lift_sup_quot_quot_mkₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
def double_quot.quot_quot_equiv_quot_supₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
((A I) J) ≃ₐ[R] A I J

`quot_quot_to_quot_add` and `lift_sup_quot_quot_mk` are inverse isomorphisms. In the case where `I ≤ J`, this is the Third Isomorphism Theorem (see `quot_quot_equiv_quot_of_le`).

Equations
@[simp]
theorem double_quot.quot_quot_equiv_quot_supₐ_to_ring_equiv (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.coe_quot_quot_equiv_quot_supₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.quot_quot_equiv_quot_supₐ_symm_to_ring_equiv (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.coe_quot_quot_equiv_quot_supₐ_symm (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
def double_quot.quot_quot_equiv_commₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
((A I) J) ≃ₐ[R] (A J) I

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
@[simp]
theorem double_quot.quot_quot_equiv_commₐ_to_ring_equiv (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.coe_quot_quot_equiv_commₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.quot_quot_equiv_comm_symmₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
@[simp]
theorem double_quot.quot_quot_equiv_comm_comp_quot_quot_mkₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] (I J : ideal A) :
J) =
def double_quot.quot_quot_equiv_quot_of_leₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] {I J : ideal A} (h : I J) :
((A I) J) ≃ₐ[R] A J

The third isomoprhism theorem for rings. See `quot_quot_equiv_quot_sup` for version that does not assume an inclusion of ideals.

Equations
@[simp]
theorem double_quot.quot_quot_equiv_quot_of_leₐ_to_ring_equiv (R : Type u) {A : Type u_1} [comm_ring A] [ A] {I J : ideal A} (h : I J) :
@[simp]
theorem double_quot.coe_quot_quot_equiv_quot_of_leₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] {I J : ideal A} (h : I J) :
@[simp]
theorem double_quot.quot_quot_equiv_quot_of_leₐ_symm_to_ring_equiv (R : Type u) {A : Type u_1} [comm_ring A] [ A] {I J : ideal A} (h : I J) :
@[simp]
theorem double_quot.coe_quot_quot_equiv_quot_of_leₐ_symm (R : Type u) {A : Type u_1} [comm_ring A] [ A] {I J : ideal A} (h : I J) :
@[simp]
theorem double_quot.quot_quot_equiv_quot_of_le_comp_quot_quot_mkₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] {I J : ideal A} (h : I J) :
@[simp]
theorem double_quot.quot_quot_equiv_quot_of_le_symm_comp_mkₐ (R : Type u) {A : Type u_1} [comm_ring A] [ A] {I J : ideal A} (h : I J) :
=