# More operations on modules and ideals related to quotients #

## Main results: #

• RingHom.quotientKerEquivRange : the first isomorphism theorem for commutative rings.
• RingHom.quotientKerEquivRangeS : the first isomorphism theorem for a morphism from a commutative ring to a semiring.
• AlgHom.quotientKerEquivRange : the first isomorphism theorem for a morphism of algebras (over a commutative semiring)
• RingHom.quotientKerEquivRangeS : the first isomorphism theorem for a morphism from a commutative ring to a semiring.
• Ideal.quotientInfRingEquivPiQuotient: the Chinese Remainder Theorem, version for coprime ideals (see also ZMod.prodEquivPi in Data.ZMod.Quotient for elementary versions about ZMod).
def RingHom.kerLift {R : Type u} {S : Type v} [] [] (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
• f.kerLift =
Instances For
@[simp]
theorem RingHom.kerLift_mk {R : Type u} {S : Type v} [] [] (f : R →+* S) (r : R) :
f.kerLift (() r) = f r
theorem RingHom.lift_injective_of_ker_le_ideal {R : Type u} {S : Type v} [] [] (I : ) {f : R →+* S} (H : aI, f a = 0) (hI : I) :
theorem RingHom.kerLift_injective {R : Type u} {S : Type v} [] [] (f : R →+* S) :
Function.Injective f.kerLift

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

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

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]
theorem RingHom.quotientKerEquivOfRightInverse.apply {R : Type u} {S : Type v} [] [] {f : R →+* S} {g : SR} (hf : ) (x : R ) :
= f.kerLift x
@[simp]
theorem RingHom.quotientKerEquivOfRightInverse.Symm.apply {R : Type u} {S : Type v} [] [] {f : R →+* S} {g : SR} (hf : ) (x : S) :
.symm x = () (g x)
def RingEquiv.quotientBot (R : Type u) [] :

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} [] [] {f : R →+* S} (hf : ) :

The first isomorphism theorem for commutative rings, surjective case.

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

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

Equations
• f.quotientKerEquivRangeS = .trans
Instances For
noncomputable def RingHom.quotientKerEquivRange {R : Type u} [] {S : Type v} [Ring S] (f : R →+* S) :
R ≃+* f.range

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

Equations
• f.quotientKerEquivRange = .trans
Instances For
@[simp]
theorem Ideal.map_quotient_self {R : Type u} [] (I : ) :
@[simp]
theorem Ideal.mk_ker {R : Type u} [] {I : } :
theorem Ideal.map_mk_eq_bot_of_le {R : Type u} [] {I : } {J : } (h : I J) :
theorem Ideal.ker_quotient_lift {R : Type u} {S : Type v} [] [] {I : } (f : R →+* S) (H : I ) :
theorem Ideal.injective_lift_iff {R : Type u} {S : Type v} [] [] {I : } {f : R →+* S} (H : aI, f a = 0) :
= I
theorem Ideal.ker_Pi_Quotient_mk {R : Type u} [] {ι : Type u_1} (I : ι) :
RingHom.ker (Pi.ringHom fun (i : ι) => Ideal.Quotient.mk (I i)) = ⨅ (i : ι), I i
@[simp]
theorem Ideal.bot_quotient_isMaximal_iff {R : Type u} [] (I : ) :
.IsMaximal I.IsMaximal
@[simp]
theorem Ideal.mem_quotient_iff_mem_sup {R : Type u} [] {I : } {J : } {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} [] {I : } {J : } (hIJ : I J) {x : R} :
x x J

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

def Ideal.quotientInfToPiQuotient {R : Type u} [] {ι : Type u_1} (I : ι) :
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} [] {ι : Type u_1} (I : ι) (x : R) :
((Ideal.Quotient.mk (⨅ (i : ι), I i)) x) = fun (i : ι) => (Ideal.Quotient.mk (I i)) x
theorem Ideal.quotientInfToPiQuotient_mk' {R : Type u} [] {ι : Type u_1} (I : ι) (x : R) (i : ι) :
((Ideal.Quotient.mk (⨅ (i : ι), I i)) x) i = (Ideal.Quotient.mk (I i)) x
theorem Ideal.quotientInfToPiQuotient_inj {R : Type u} [] {ι : Type u_1} (I : ι) :
theorem Ideal.quotientInfToPiQuotient_surj {R : Type u} [] {ι : Type u_1} [] {I : ι} (hI : Pairwise fun (i j : ι) => IsCoprime (I i) (I j)) :
noncomputable def Ideal.quotientInfRingEquivPiQuotient {R : Type u} [] {ι : Type u_1} [] (f : ι) (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
theorem Ideal.pi_quotient_surjective {R : Type u_2} [] {ι : Type u_3} [] {I : ι} (hf : Pairwise fun (i j : ι) => IsCoprime (I i) (I j)) (x : (i : ι) → R I i) :
∃ (r : R), ∀ (i : ι), (Ideal.Quotient.mk (I i)) r = x i

Corollary of Chinese Remainder Theorem: if Iᵢ are pairwise coprime ideals in a commutative ring then the canonical map R → ∏ (R ⧸ Iᵢ) is surjective.

theorem Ideal.exists_forall_sub_mem_ideal {R : Type u_2} [] {ι : Type u_3} [] {I : ι} (hI : Pairwise fun (i j : ι) => IsCoprime (I i) (I j)) (x : ιR) :
∃ (r : R), ∀ (i : ι), r - x i I i

Corollary of Chinese Remainder Theorem: if Iᵢ are pairwise coprime ideals in a commutative ring then given elements xᵢ you can find r with r - xᵢ ∈ Iᵢ for all i.

noncomputable def Ideal.quotientInfEquivQuotientProd {R : Type u} [] (I : ) (J : ) (coprime : ) :
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} [] (I : ) (J : ) (coprime : ) (x : R I J) :
((I.quotientInfEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor (I J) I ) x
@[simp]
theorem Ideal.quotientInfEquivQuotientProd_snd {R : Type u} [] (I : ) (J : ) (coprime : ) (x : R I J) :
((I.quotientInfEquivQuotientProd J coprime) x).2 = (Ideal.Quotient.factor (I J) J ) x
@[simp]
theorem Ideal.fst_comp_quotientInfEquivQuotientProd {R : Type u} [] (I : ) (J : ) (coprime : ) :
(RingHom.fst (R I) (R J)).comp (I.quotientInfEquivQuotientProd J coprime) = Ideal.Quotient.factor (I J) I
@[simp]
theorem Ideal.snd_comp_quotientInfEquivQuotientProd {R : Type u} [] (I : ) (J : ) (coprime : ) :
(RingHom.snd (R I) (R J)).comp (I.quotientInfEquivQuotientProd J coprime) = Ideal.Quotient.factor (I J) J
noncomputable def Ideal.quotientMulEquivQuotientProd {R : Type u} [] (I : ) (J : ) (coprime : ) :
R I * J ≃+* (R I) × R J

Chinese remainder theorem, specialized to two ideals.

Equations
• I.quotientMulEquivQuotientProd J coprime = .trans (I.quotientInfEquivQuotientProd J coprime)
Instances For
@[simp]
theorem Ideal.quotientMulEquivQuotientProd_fst {R : Type u} [] (I : ) (J : ) (coprime : ) (x : R I * J) :
((I.quotientMulEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor (I * J) I ) x
@[simp]
theorem Ideal.quotientMulEquivQuotientProd_snd {R : Type u} [] (I : ) (J : ) (coprime : ) (x : R I * J) :
((I.quotientMulEquivQuotientProd J coprime) x).2 = (Ideal.Quotient.factor (I * J) J ) x
@[simp]
theorem Ideal.fst_comp_quotientMulEquivQuotientProd {R : Type u} [] (I : ) (J : ) (coprime : ) :
(RingHom.fst (R I) (R J)).comp (I.quotientMulEquivQuotientProd J coprime) = Ideal.Quotient.factor (I * J) I
@[simp]
theorem Ideal.snd_comp_quotientMulEquivQuotientProd {R : Type u} [] (I : ) (J : ) (coprime : ) :
(RingHom.snd (R I) (R J)).comp (I.quotientMulEquivQuotientProd J coprime) = Ideal.Quotient.factor (I * J) J
instance Ideal.Quotient.algebra (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] {I : } :
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} [] [] [] [Algebra R₁ A] [Algebra R₂ A] [SMul R₁ R₂] [IsScalarTower R₁ R₂ A] (I : ) :
IsScalarTower R₁ R₂ (A I)
Equations
• =
def Ideal.Quotient.mkₐ (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] (I : ) :
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
• = { toFun := fun (a : A) => , map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
theorem Ideal.Quotient.algHom_ext (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] {I : } {S : Type u_5} [] [Algebra R₁ S] ⦃f : A I →ₐ[R₁] S ⦃g : A I →ₐ[R₁] S (h : f.comp () = g.comp ()) :
f = g
theorem Ideal.Quotient.alg_map_eq (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] (I : ) :
algebraMap R₁ (A I) = (algebraMap A (A I)).comp (algebraMap R₁ A)
theorem Ideal.Quotient.mkₐ_toRingHom (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] (I : ) :
().toRingHom =
@[simp]
theorem Ideal.Quotient.mkₐ_eq_mk (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] (I : ) :
() =
@[simp]
theorem Ideal.Quotient.algebraMap_eq {R : Type u} [] (I : ) :
algebraMap R (R I) =
@[simp]
theorem Ideal.Quotient.mk_comp_algebraMap (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] (I : ) :
.comp (algebraMap R₁ A) = algebraMap R₁ (A I)
@[simp]
theorem Ideal.Quotient.mk_algebraMap (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] (I : ) (x : R₁) :
((algebraMap R₁ A) x) = (algebraMap R₁ (A I)) x
theorem Ideal.Quotient.mkₐ_surjective (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] (I : ) :

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

@[simp]
theorem Ideal.Quotient.mkₐ_ker (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] (I : ) :
RingHom.ker () = 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} [] [] [Algebra R₁ A] [] [Algebra R₁ B] (I : ) (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} [] [] [Algebra R₁ A] [] [Algebra R₁ B] (I : ) (f : A →ₐ[R₁] B) (hI : aI, f a = 0) (x : A I) :
() 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} [] [] [Algebra R₁ A] [] [Algebra R₁ B] (I : ) (f : A →ₐ[R₁] B) (hI : aI, f a = 0) :
().comp () = f
theorem Ideal.KerLift.map_smul {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] (f : A →ₐ[R₁] B) (r : R₁) (x : A ) :
f.kerLift (r x) = r f.kerLift x
def Ideal.kerLiftAlg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] (f : A →ₐ[R₁] B) :
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} [] [] [Algebra R₁ A] [] [Algebra R₁ B] (f : A →ₐ[R₁] B) (a : A) :
() (() a) = f a
@[simp]
theorem Ideal.kerLiftAlg_toRingHom {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] (f : A →ₐ[R₁] B) :
() = (f).kerLift
theorem Ideal.kerLiftAlg_injective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [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} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : ) :
∀ (a : B), .symm a = () (g a)
@[simp]
theorem Ideal.quotientKerAlgEquivOfRightInverse_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : ) (a : A RingHom.ker f.toRingHom) :
= (f).kerLift a
def Ideal.quotientKerAlgEquivOfRightInverse {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : ) :
(A ) ≃ₐ[R₁] B

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} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : ) (a : A RingHom.ker f.toRingHom) :
= (f).kerLift a

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} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : BA} (hf : ) :
∀ (a : B), .symm a = () (g a)

Alias of Ideal.quotientKerAlgEquivOfRightInverse_symm_apply.

@[simp]
theorem Ideal.quotientKerAlgEquivOfSurjective_symm_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : ) :
∀ (a : B), .symm a = () ()
@[simp]
theorem Ideal.quotientKerAlgEquivOfSurjective_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : ) (a : A RingHom.ker f.toRingHom) :
= (f).kerLift a
noncomputable def Ideal.quotientKerAlgEquivOfSurjective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : ) :
(A ) ≃ₐ[R₁] B

The first isomorphism theorem for algebras.

Equations
Instances For
def Ideal.quotientMap {R : Type u} [] {S : Type v} [] {I : } (J : ) (f : R →+* S) (hIJ : I ) :
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} [] {S : Type v} [] {J : } {I : } {f : R →+* S} {H : J } {x : R} :
() ( x) = (f x)
@[simp]
theorem Ideal.quotientMap_algebraMap {R₁ : Type u_1} {A : Type u_3} [] [] [Algebra R₁ A] {S : Type v} [] {J : } {I : } {f : A →+* S} {H : J } {x : R₁} :
() ((algebraMap R₁ (A J)) x) = (f ((algebraMap R₁ A) x))
theorem Ideal.quotientMap_comp_mk {R : Type u} [] {S : Type v} [] {J : } {I : } {f : R →+* S} (H : J ) :
().comp = .comp f
@[simp]
theorem Ideal.quotientEquiv_symm_apply {R : Type u} [] {S : Type v} [] (I : ) (J : ) (f : R ≃+* S) (hIJ : J = Ideal.map (f) I) (a : S J) :
(I.quotientEquiv J f hIJ).symm a = (Ideal.quotientMap I f.symm ) a
@[simp]
theorem Ideal.quotientEquiv_apply {R : Type u} [] {S : Type v} [] (I : ) (J : ) (f : R ≃+* S) (hIJ : J = Ideal.map (f) I) :
∀ (a : R I), (I.quotientEquiv J f hIJ) a = (()).toFun a
def Ideal.quotientEquiv {R : Type u} [] {S : Type v} [] (I : ) (J : ) (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} [] {S : Type v} [] (I : ) (J : ) (f : R ≃+* S) (hIJ : J = Ideal.map (f) I) (x : R) :
(I.quotientEquiv J f hIJ) ( x) = (f x)
@[simp]
theorem Ideal.quotientEquiv_symm_mk {R : Type u} [] {S : Type v} [] (I : ) (J : ) (f : R ≃+* S) (hIJ : J = Ideal.map (f) I) (x : S) :
(I.quotientEquiv J f hIJ).symm ( x) = (f.symm x)
theorem Ideal.quotientMap_injective' {R : Type u} [] {S : Type v} [] {J : } {I : } {f : R →+* S} {H : J } (h : 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} [] {S : Type v} [] {I : } {f : R →+* S} :

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

theorem Ideal.quotientMap_surjective {R : Type u} [] {S : Type v} [] {J : } {I : } {f : R →+* S} {H : J } (hf : ) :
theorem Ideal.comp_quotientMap_eq_of_comp_eq {R : Type u} [] {S : Type v} [] {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 : f'.comp g = g'.comp f) (I : Ideal S') :
let leq := ; ().comp (Ideal.quotientMap (Ideal.comap g' I) f ) = ().comp (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} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {I : } (J : ) (f : A →ₐ[R₁] B) (hIJ : I ) :
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} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {I : } (J : ) (f : A →ₐ[R₁] B) (H : I ) {x : A} :
() ( x) = () (f x)
theorem Ideal.quotient_map_comp_mkₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] {I : } (J : ) (f : A →ₐ[R₁] B) (H : I ) :
().comp () = ().comp f
def Ideal.quotientEquivAlg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [Algebra R₁ A] [] [Algebra R₁ B] (I : ) (J : ) (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
• I.quotientEquivAlg J f hIJ = let __src := I.quotientEquiv J (f) hIJ; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
@[instance 100]
instance Ideal.quotientAlgebra {R : Type u} [] {A : Type u_3} [] {I : } [Algebra R A] :
Algebra (R Ideal.comap () I) (A I)
Equations
theorem Ideal.algebraMap_quotient_injective {R : Type u} [] {A : Type u_3} [] {I : } [Algebra R A] :
def Ideal.quotientEquivAlgOfEq (R₁ : Type u_1) {A : Type u_3} [] [] [Algebra R₁ A] {I : } {J : } (h : I = J) :
(A I) ≃ₐ[R₁] A J

Quotienting by equal ideals gives equivalent algebras.

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

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

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

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

Equations
Instances For
theorem DoubleQuot.ker_quotLeftToQuotSup {R : Type u} [] (I : ) (J : ) :

The kernel of quotLeftToQuotSup

def DoubleQuot.quotQuotToQuotSup {R : Type u} [] (I : ) (J : ) :
(R I) →+* 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

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

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

Equations
• = ().comp
Instances For
theorem DoubleQuot.ker_quotQuotMk {R : Type u} [] (I : ) (J : ) :
= I J

The kernel of quotQuotMk

def DoubleQuot.liftSupQuotQuotMk {R : Type u} [] (I : ) (J : ) :
R I J →+* (R I)

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

Equations
Instances For
def DoubleQuot.quotQuotEquivQuotSup {R : Type u} [] (I : ) (J : ) :
(R I) ≃+* R I J

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

Equations
Instances For
@[simp]
theorem DoubleQuot.quotQuotEquivQuotSup_quotQuotMk {R : Type u} [] (I : ) (J : ) (x : R) :
(() x) = (Ideal.Quotient.mk (I J)) x
@[simp]
theorem DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk {R : Type u} [] (I : ) (J : ) (x : R) :
.symm ((Ideal.Quotient.mk (I J)) x) = () x
def DoubleQuot.quotQuotEquivComm {R : Type u} [] (I : ) (J : ) :
(R I) ≃+* (R J)

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

Equations
• = (.trans ).trans .symm
Instances For
@[simp]
theorem DoubleQuot.quotQuotEquivComm_quotQuotMk {R : Type u} [] (I : ) (J : ) (x : R) :
(() x) = () x
@[simp]
theorem DoubleQuot.quotQuotEquivComm_comp_quotQuotMk {R : Type u} [] (I : ) (J : ) :
().comp () =
@[simp]
theorem DoubleQuot.quotQuotEquivComm_symm {R : Type u} [] (I : ) (J : ) :
.symm =
def DoubleQuot.quotQuotEquivQuotOfLE {R : Type u} [] {I : } {J : } (h : I J) :
(R I) ≃+* R J

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

Equations
Instances For
@[simp]
theorem DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk {R : Type u} [] {I : } {J : } (x : R) (h : I J) :
(() x) = x
@[simp]
theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_mk {R : Type u} [] {I : } {J : } (x : R) (h : I J) :
.symm ( x) = () x
theorem DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk {R : Type u} [] {I : } {J : } (h : I J) :
.comp () =
theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk {R : Type u} [] {I : } {J : } (h : I J) :
(.symm).comp =
@[simp]
theorem DoubleQuot.quotQuotEquivComm_mk_mk {R : Type u} [] (I : ) (J : ) (x : R) :
(() ( x)) = (algebraMap R ((R J) )) x
@[simp]
theorem DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap {R : Type u} [] {A : Type v} [] [Algebra R A] (I : ) (J : ) (x : R) :
((algebraMap R ((A I) )) x) = (algebraMap R (A I J)) x
@[simp]
theorem DoubleQuot.quotQuotEquivComm_algebraMap {R : Type u} [] {A : Type v} [] [Algebra R A] (I : ) (J : ) (x : R) :
((algebraMap R ((A I) )) x) = (algebraMap R ((A J) )) x
def DoubleQuot.quotLeftToQuotSupₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
A I →ₐ[R] A I J

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

Equations
• = { toRingHom := , commutes' := }
Instances For
@[simp]
theorem DoubleQuot.quotLeftToQuotSupₐ_toRingHom (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
@[simp]
theorem DoubleQuot.coe_quotLeftToQuotSupₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
() =
def DoubleQuot.quotQuotToQuotSupₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
(A I) Ideal.map () 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.

Equations
• = { toRingHom := , commutes' := }
Instances For
@[simp]
theorem DoubleQuot.quotQuotToQuotSupₐ_toRingHom (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
@[simp]
theorem DoubleQuot.coe_quotQuotToQuotSupₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
() =
def DoubleQuot.quotQuotMkₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
A →ₐ[R] (A I) Ideal.map () 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
• = { toRingHom := , commutes' := }
Instances For
@[simp]
theorem DoubleQuot.quotQuotMkₐ_toRingHom (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
() =
@[simp]
theorem DoubleQuot.coe_quotQuotMkₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
() = ()
def DoubleQuot.liftSupQuotQuotMkₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
A I J →ₐ[R] (A I) Ideal.map () 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
• = { toRingHom := , commutes' := }
Instances For
@[simp]
theorem DoubleQuot.liftSupQuotQuotMkₐ_toRingHom (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
@[simp]
theorem DoubleQuot.coe_liftSupQuotQuotMkₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
() =
def DoubleQuot.quotQuotEquivQuotSupₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
((A I) Ideal.map () 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).

Equations
Instances For
@[simp]
theorem DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
@[simp]
theorem DoubleQuot.coe_quotQuotEquivQuotSupₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
() =
@[simp]
theorem DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
().symm = .symm
@[simp]
theorem DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
().symm = .symm
def DoubleQuot.quotQuotEquivCommₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
((A I) Ideal.map () J) ≃ₐ[R] (A J) Ideal.map () 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
Instances For
@[simp]
theorem DoubleQuot.quotQuotEquivCommₐ_toRingEquiv (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
@[simp]
theorem DoubleQuot.coe_quotQuotEquivCommₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
() =
@[simp]
theorem DoubleQuot.quotQuotEquivComm_symmₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
().symm =
@[simp]
theorem DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] (I : ) (J : ) :
(()).comp () =
def DoubleQuot.quotQuotEquivQuotOfLEₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] {I : } {J : } (h : I J) :
((A I) Ideal.map () J) ≃ₐ[R] A J

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

Equations
Instances For
@[simp]
theorem DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv (R : Type u) {A : Type u_1} [] [] [Algebra R A] {I : } {J : } (h : I J) :
@[simp]
theorem DoubleQuot.coe_quotQuotEquivQuotOfLEₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] {I : } {J : } (h : I J) :
@[simp]
theorem DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv (R : Type u) {A : Type u_1} [] [] [Algebra R A] {I : } {J : } (h : I J) :
.symm = .symm
@[simp]
theorem DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm (R : Type u) {A : Type u_1} [] [] [Algebra R A] {I : } {J : } (h : I J) :
.symm = .symm
@[simp]
theorem DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] {I : } {J : } (h : I J) :
().comp () =
@[simp]
theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ (R : Type u) {A : Type u_1} [] [] [Algebra R A] {I : } {J : } (h : I J) :
(.symm).comp () =