More operations on modules and ideals related to quotients

def RingHom.kerLift {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) : R ⧸ RingHom.ker f →+* 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).

@[simp]

theorem RingHom.kerLift_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (r : R) : ↑(RingHom.kerLift f) (↑(Ideal.Quotient.mk (RingHom.ker f)) r) = ↑f r

theorem RingHom.kerLift_injective {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) : Function.Injective ↑(RingHom.kerLift f)

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

theorem RingHom.lift_injective_of_ker_le_ideal {R : Type u} {S : Type v} [CommRing R] [CommRing S] (I : Ideal R) {f : R →+* S} (H : ∀ (a : R), a ∈ I → ↑f a = 0) (hI : RingHom.ker f ≤ I) : Function.Injective ↑(Ideal.Quotient.lift I f H)

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

The first isomorphism theorem for commutative rings, computable version.

@[simp]

theorem RingHom.quotientKerEquivOfRightInverse.apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} {g : S → R} (hf : Function.RightInverse g ↑f) (x : R ⧸ RingHom.ker f) : ↑(RingHom.quotientKerEquivOfRightInverse hf) x = ↑(RingHom.kerLift f) x

@[simp]

theorem RingHom.quotientKerEquivOfRightInverse.Symm.apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} {g : S → R} (hf : Function.RightInverse g ↑f) (x : S) : ↑(RingEquiv.symm (RingHom.quotientKerEquivOfRightInverse hf)) x = ↑(Ideal.Quotient.mk (RingHom.ker f)) (g x)

noncomputable def RingHom.quotientKerEquivOfSurjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ↑f) : R ⧸ RingHom.ker f ≃+* S

The first isomorphism theorem for commutative rings.

@[simp]

theorem Ideal.map_quotient_self {R : Type u} [CommRing R] (I : Ideal R) : Ideal.map (Ideal.Quotient.mk I) I = ⊥

@[simp]

theorem Ideal.mk_ker {R : Type u} [CommRing R] {I : Ideal R} : RingHom.ker (Ideal.Quotient.mk I) = I

theorem Ideal.map_mk_eq_bot_of_le {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I ≤ J) : Ideal.map (Ideal.Quotient.mk J) I = ⊥

theorem Ideal.ker_quotient_lift {R : Type u} [CommRing R] {S : Type v} [CommRing S] {I : Ideal R} (f : R →+* S) (H : I ≤ RingHom.ker f) : RingHom.ker (Ideal.Quotient.lift I f H) = Ideal.map (Ideal.Quotient.mk I) (RingHom.ker f)

@[simp]

theorem Ideal.bot_quotient_isMaximal_iff {R : Type u} [CommRing R] (I : Ideal R) : Ideal.IsMaximal ⊥ ↔ Ideal.IsMaximal I

@[simp]

theorem Ideal.mem_quotient_iff_mem_sup {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} {x : R} : ↑(Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J ⊔ I

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} : ↑(Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J

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

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

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)

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.

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) : ↑(Ideal.Quotient.mkₐ R₁ I) = Ideal.Quotient.mk I

@[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) : ↑(Ideal.Quotient.mkₐ R₁ I) = ↑(Ideal.Quotient.mk I)

@[simp]

theorem Ideal.Quotient.algebraMap_eq {R : Type u} [CommRing R] (I : Ideal R) : algebraMap R (R ⧸ I) = Ideal.Quotient.mk I

@[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) : RingHom.comp (Ideal.Quotient.mk I) (algebraMap R₁ A) = algebraMap R₁ (A ⧸ I)

@[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) : Function.Surjective ↑(Ideal.Quotient.mkₐ R₁ I)

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) : RingHom.ker ↑(Ideal.Quotient.mkₐ R₁ I) = 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} [CommSemiring R₁] [CommRing A] [CommRing 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 AlgHom.

@[simp]

theorem Ideal.Quotient.liftₐ_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing 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) : ↑(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] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] (I : Ideal A) (f : A →ₐ[R₁] B) (hI : ∀ (a : A), a ∈ I → ↑f a = 0) : AlgHom.comp (Ideal.Quotient.liftₐ I f hI) (Ideal.Quotient.mkₐ R₁ I) = f

theorem Ideal.KerLift.map_smul {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] (f : A →ₐ[R₁] B) (r : R₁) (x : A ⧸ RingHom.ker ↑f) : ↑(RingHom.kerLift ↑f) (r • x) = r • ↑(RingHom.kerLift ↑f) x

def Ideal.kerLiftAlg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] (f : A →ₐ[R₁] B) : A ⧸ RingHom.ker ↑f →ₐ[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).

@[simp]

theorem Ideal.kerLiftAlg_mk {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] (f : A →ₐ[R₁] B) (a : A) : ↑(Ideal.kerLiftAlg f) (↑(Ideal.Quotient.mk (RingHom.ker f)) a) = ↑f a

@[simp]

theorem Ideal.kerLiftAlg_toRingHom {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] (f : A →ₐ[R₁] B) : ↑(Ideal.kerLiftAlg f) = RingHom.kerLift ↑f

theorem Ideal.kerLiftAlg_injective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] (f : A →ₐ[R₁] B) : Function.Injective ↑(Ideal.kerLiftAlg f)

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

def Ideal.quotientKerAlgEquivOfRightInverse {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ↑f) : (A ⧸ RingHom.ker ↑f) ≃ₐ[R₁] B

The first isomorphism theorem for algebras, computable version.

@[simp]

theorem Ideal.quotientKerAlgEquivOfRightInverse.apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ↑f) (x : A ⧸ RingHom.ker ↑f) : ↑(Ideal.quotientKerAlgEquivOfRightInverse hf) x = ↑(Ideal.kerLiftAlg f) x

@[simp]

theorem Ideal.QuotientKerAlgEquivOfRightInverseSymm.apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ↑f) (x : B) : ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfRightInverse hf)) x = ↑(Ideal.Quotient.mkₐ R₁ (RingHom.ker ↑f)) (g x)

noncomputable def Ideal.quotientKerAlgEquivOfSurjective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective ↑f) : (A ⧸ RingHom.ker ↑f) ≃ₐ[R₁] B

The first isomorphism theorem for algebras.

def Ideal.quotientMap {R : Type u} {S : Type v} [CommRing R] [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)

@[simp]

theorem Ideal.quotientMap_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} {H : J ≤ Ideal.comap f I} {x : R} : ↑(Ideal.quotientMap I f H) (↑(Ideal.Quotient.mk J) x) = ↑(Ideal.Quotient.mk I) (↑f x)

@[simp]

theorem Ideal.quotientMap_algebraMap {S : Type v} [CommRing S] {R₁ : Type u_1} {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {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))

theorem Ideal.quotientMap_comp_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} (H : J ≤ Ideal.comap f I) : RingHom.comp (Ideal.quotientMap I f H) (Ideal.Quotient.mk J) = RingHom.comp (Ideal.Quotient.mk I) f

@[simp]

theorem Ideal.quotientEquiv_apply {R : Type u} {S : Type v} [CommRing R] [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 = OneHom.toFun (↑↑(Ideal.quotientMap J ↑f (_ : I ≤ Ideal.comap (↑f) J))) a

@[simp]

theorem Ideal.quotientEquiv_symm_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (a : S ⧸ J) : ↑(RingEquiv.symm (Ideal.quotientEquiv I J f hIJ)) a = ↑(Ideal.quotientMap I ↑(RingEquiv.symm f) (_ : J ≤ Ideal.comap (↑(RingEquiv.symm f)) I)) a

def Ideal.quotientEquiv {R : Type u} {S : Type v} [CommRing R] [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).

theorem Ideal.quotientEquiv_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (x : R) : ↑(Ideal.quotientEquiv I J f hIJ) (↑(Ideal.Quotient.mk I) x) = ↑(Ideal.Quotient.mk J) (↑f x)

@[simp]

theorem Ideal.quotientEquiv_symm_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (x : S) : ↑(RingEquiv.symm (Ideal.quotientEquiv I J f hIJ)) (↑(Ideal.Quotient.mk J) x) = ↑(Ideal.Quotient.mk I) (↑(RingEquiv.symm f) x)

theorem Ideal.quotientMap_injective' {R : Type u} {S : Type v} [CommRing R] [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} {H : J ≤ Ideal.comap f I} (h : Ideal.comap f I ≤ J) : Function.Injective ↑(Ideal.quotientMap I f H)

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

theorem Ideal.quotientMap_injective {R : Type u} {S : Type v} [CommRing R] [CommRing S] {I : Ideal S} {f : R →+* S} : Function.Injective ↑(Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I))

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

theorem Ideal.quotientMap_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} {H : J ≤ Ideal.comap f I} (hf : Function.Surjective ↑f) : Function.Surjective ↑(Ideal.quotientMap I f H)

theorem Ideal.comp_quotientMap_eq_of_comp_eq {R : Type u} {S : Type v} [CommRing R] [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') : let leq := (_ : Ideal.comap f (Ideal.comap g' I) ≤ Ideal.comap g (Ideal.comap f' I)); RingHom.comp (Ideal.quotientMap I g' (_ : Ideal.comap g' I ≤ Ideal.comap g' I)) (Ideal.quotientMap (Ideal.comap g' I) f (_ : Ideal.comap f (Ideal.comap g' I) ≤ Ideal.comap f (Ideal.comap g' I))) = RingHom.comp (Ideal.quotientMap I f' (_ : Ideal.comap f' I ≤ Ideal.comap f' I)) (Ideal.quotientMap (Ideal.comap f' I) g leq)

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] [CommRing B] [Algebra R₁ A] [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).

@[simp]

theorem Ideal.quotient_map_mkₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] {I : Ideal A} (J : Ideal B) (f : A →ₐ[R₁] B) (H : I ≤ Ideal.comap f J) {x : A} : ↑(Ideal.quotientMapₐ J f H) (↑(Ideal.Quotient.mk I) x) = ↑(Ideal.Quotient.mkₐ R₁ J) (↑f x)

theorem Ideal.quotient_map_comp_mkₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [Algebra R₁ B] {I : Ideal A} (J : Ideal B) (f : A →ₐ[R₁] B) (H : I ≤ Ideal.comap f J) : AlgHom.comp (Ideal.quotientMapₐ J f H) (Ideal.Quotient.mkₐ R₁ I) = AlgHom.comp (Ideal.Quotient.mkₐ R₁ J) f

def Ideal.quotientEquivAlg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [CommRing B] [Algebra R₁ A] [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).

instance Ideal.quotientAlgebra {R : Type u} [CommRing R] {A : Type u_3} [CommRing A] {I : Ideal A} [Algebra R A] : Algebra (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I)

theorem Ideal.algebraMap_quotient_injective {R : Type u} [CommRing R] {A : Type u_3} [CommRing A] {I : Ideal A} [Algebra R A] : Function.Injective ↑(algebraMap (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I))

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.

@[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) : ↑(Ideal.quotientEquivAlgOfEq R₁ h) (↑(Ideal.Quotient.mk I) x) = ↑(Ideal.Quotient.mk J) x

@[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) : AlgEquiv.symm (Ideal.quotientEquivAlgOfEq R₁ h) = Ideal.quotientEquivAlgOfEq R₁ (_ : J = I)

theorem Ideal.comap_map_mk {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I ≤ J) : Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = J

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)

theorem DoubleQuot.ker_quotLeftToQuotSup {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) : RingHom.ker (DoubleQuot.quotLeftToQuotSup I J) = Ideal.map (Ideal.Quotient.mk I) J

The kernel of quotLeftToQuotSup

def DoubleQuot.quotQuotToQuotSup {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →+* R ⧸ I ⊔ J

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

def DoubleQuot.quotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) : R →+* (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J

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

theorem DoubleQuot.ker_quotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) : RingHom.ker (DoubleQuot.quotQuotMk I J) = I ⊔ J

The kernel of quotQuotMk

def DoubleQuot.liftSupQuotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) : R ⧸ I ⊔ J →+* (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J

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

def DoubleQuot.quotQuotEquivQuotSup {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* R ⧸ I ⊔ J

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

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSup_quotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (x : R) : ↑(DoubleQuot.quotQuotEquivQuotSup I J) (↑(DoubleQuot.quotQuotMk I J) x) = ↑(Ideal.Quotient.mk (I ⊔ J)) x

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (x : R) : ↑(RingEquiv.symm (DoubleQuot.quotQuotEquivQuotSup I J)) (↑(Ideal.Quotient.mk (I ⊔ J)) x) = ↑(DoubleQuot.quotQuotMk I J) x

def DoubleQuot.quotQuotEquivComm {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* (R ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I

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

@[simp]

theorem DoubleQuot.quotQuotEquivComm_quotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (x : R) : ↑(DoubleQuot.quotQuotEquivComm I J) (↑(DoubleQuot.quotQuotMk I J) x) = ↑(DoubleQuot.quotQuotMk J I) x

@[simp]

theorem DoubleQuot.quotQuotEquivComm_comp_quotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) : RingHom.comp (↑(DoubleQuot.quotQuotEquivComm I J)) (DoubleQuot.quotQuotMk I J) = DoubleQuot.quotQuotMk J I

@[simp]

theorem DoubleQuot.quotQuotEquivComm_symm {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) : RingEquiv.symm (DoubleQuot.quotQuotEquivComm I J) = DoubleQuot.quotQuotEquivComm J I

def DoubleQuot.quotQuotEquivQuotOfLE {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I ≤ J) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* R ⧸ J

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

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (x : R) (h : I ≤ J) : ↑(DoubleQuot.quotQuotEquivQuotOfLE h) (↑(DoubleQuot.quotQuotMk I J) x) = ↑(Ideal.Quotient.mk J) x

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_mk {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (x : R) (h : I ≤ J) : ↑(RingEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLE h)) (↑(Ideal.Quotient.mk J) x) = ↑(DoubleQuot.quotQuotMk I J) x

theorem DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I ≤ J) : RingHom.comp (↑(DoubleQuot.quotQuotEquivQuotOfLE h)) (DoubleQuot.quotQuotMk I J) = Ideal.Quotient.mk J

theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I ≤ J) : RingHom.comp (↑(RingEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLE h))) (Ideal.Quotient.mk J) = DoubleQuot.quotQuotMk I J

@[simp]

theorem DoubleQuot.quotQuotEquivComm_mk_mk {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (x : R) : ↑(DoubleQuot.quotQuotEquivComm I J) (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) (↑(Ideal.Quotient.mk I) x)) = ↑(algebraMap R ((R ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap {R : Type u} [CommSemiring R] {A : Type v} [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) (x : R) : ↑(DoubleQuot.quotQuotEquivQuotSup I J) (↑(algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) = ↑(algebraMap R (A ⧸ I ⊔ J)) x

@[simp]

theorem DoubleQuot.quotQuotEquivComm_algebraMap {R : Type u} [CommSemiring R] {A : Type v} [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) (x : R) : ↑(DoubleQuot.quotQuotEquivComm I J) (↑(algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) = ↑(algebraMap R ((A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x

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).

@[simp]

theorem DoubleQuot.quotLeftToQuotSupₐ_toRingHom (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.quotLeftToQuotSupₐ R I J) = DoubleQuot.quotLeftToQuotSup I J

@[simp]

theorem DoubleQuot.coe_quotLeftToQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.quotLeftToQuotSupₐ R I J) = ↑(DoubleQuot.quotLeftToQuotSup I J)

def DoubleQuot.quotQuotToQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J →ₐ[R] A ⧸ I ⊔ J

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

@[simp]

theorem DoubleQuot.quotQuotToQuotSupₐ_toRingHom (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.quotQuotToQuotSupₐ R I J) = DoubleQuot.quotQuotToQuotSup I J

@[simp]

theorem DoubleQuot.coe_quotQuotToQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.quotQuotToQuotSupₐ R I J) = ↑(DoubleQuot.quotQuotToQuotSup I J)

def DoubleQuot.quotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : A →ₐ[R] (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R 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.

@[simp]

theorem DoubleQuot.quotQuotMkₐ_toRingHom (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMk I J

@[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) : ↑(DoubleQuot.quotQuotMkₐ R I J) = ↑(DoubleQuot.quotQuotMk I J)

def DoubleQuot.liftSupQuotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : A ⧸ I ⊔ J →ₐ[R] (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R 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.

@[simp]

theorem DoubleQuot.liftSupQuotQuotMkₐ_toRingHom (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = DoubleQuot.liftSupQuotQuotMk I J

@[simp]

theorem DoubleQuot.coe_liftSupQuotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = ↑(DoubleQuot.liftSupQuotQuotMk I J)

def DoubleQuot.quotQuotEquivQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] A ⧸ I ⊔ J

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

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.quotQuotEquivQuotSupₐ R I J) = DoubleQuot.quotQuotEquivQuotSup I J

@[simp]

theorem DoubleQuot.coe_quotQuotEquivQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.quotQuotEquivQuotSupₐ R I J) = ↑(DoubleQuot.quotQuotEquivQuotSup I J)

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotSupₐ R I J)) = RingEquiv.symm (DoubleQuot.quotQuotEquivQuotSup I J)

@[simp]

theorem DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotSupₐ R I J)) = ↑(RingEquiv.symm (DoubleQuot.quotQuotEquivQuotSup I J))

def DoubleQuot.quotQuotEquivCommₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] (A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mkₐ R 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).

@[simp]

theorem DoubleQuot.quotQuotEquivCommₐ_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.quotQuotEquivCommₐ R I J) = DoubleQuot.quotQuotEquivComm I J

@[simp]

theorem DoubleQuot.coe_quotQuotEquivCommₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : ↑(DoubleQuot.quotQuotEquivCommₐ R I J) = ↑(DoubleQuot.quotQuotEquivComm I J)

@[simp]

theorem DoubleQuot.quotQuotEquivComm_symmₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : AlgEquiv.symm (DoubleQuot.quotQuotEquivCommₐ R I J) = DoubleQuot.quotQuotEquivCommₐ R J I

@[simp]

theorem DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I : Ideal A) (J : Ideal A) : AlgHom.comp (↑(DoubleQuot.quotQuotEquivCommₐ R I J)) (DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMkₐ R J I

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) : ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] A ⧸ J

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

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I : Ideal A} {J : Ideal A} (h : I ≤ J) : ↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h) = DoubleQuot.quotQuotEquivQuotOfLE h

@[simp]

theorem DoubleQuot.coe_quotQuotEquivQuotOfLEₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I : Ideal A} {J : Ideal A} (h : I ≤ J) : ↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h) = ↑(DoubleQuot.quotQuotEquivQuotOfLE h)

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I : Ideal A} {J : Ideal A} (h : I ≤ J) : ↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R h)) = RingEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLE h)

@[simp]

theorem DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I : Ideal A} {J : Ideal A} (h : I ≤ J) : ↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R h)) = ↑(RingEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLE h))

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I : Ideal A} {J : Ideal A} (h : I ≤ J) : AlgHom.comp (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h)) (DoubleQuot.quotQuotMkₐ R I J) = Ideal.Quotient.mkₐ R J

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I : Ideal A} {J : Ideal A} (h : I ≤ J) : AlgHom.comp (↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R h))) (Ideal.Quotient.mkₐ R J) = DoubleQuot.quotQuotMkₐ R I J