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 alsoZMod.prodEquivPi
inData.ZMod.Quotient
for elementary versions aboutZMod
).
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 = Ideal.Quotient.lift (RingHom.ker f) f ⋯
The induced map from the quotient by the kernel is injective.
The first isomorphism theorem for commutative rings, computable version.
Equations
- RingHom.quotientKerEquivOfRightInverse hf = { toFun := ⇑f.kerLift, invFun := ⇑(Ideal.Quotient.mk (RingHom.ker f)) ∘ g, left_inv := ⋯, right_inv := hf, map_mul' := ⋯, map_add' := ⋯ }
The quotient of a ring by he zero ideal is isomorphic to the ring itself.
Equations
The first isomorphism theorem for commutative rings, surjective case.
The first isomorphism theorem for commutative rings (RingHom.rangeS
version).
Equations
- f.quotientKerEquivRangeS = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)
The first isomorphism theorem for commutative rings (RingHom.range
version).
Equations
- f.quotientKerEquivRange = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)
See also Ideal.mem_quotient_iff_mem
in case I ≤ J
.
See also Ideal.mem_quotient_iff_mem_sup
if the assumption I ≤ J
is not available.
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
- Ideal.quotientInfToPiQuotient I = Ideal.Quotient.lift (⨅ (i : ι), I i) (Pi.ringHom fun (i : ι) => Ideal.Quotient.mk (I i)) ⋯
Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT
Equations
- Ideal.quotientInfRingEquivPiQuotient f hf = { toEquiv := Equiv.ofBijective ⇑(Ideal.quotientInfToPiQuotient f) ⋯, map_mul' := ⋯, map_add' := ⋯ }
Corollary of Chinese Remainder Theorem: if Iᵢ
are pairwise coprime ideals in a
commutative ring then the canonical map R → ∏ (R ⧸ Iᵢ)
is surjective.
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
.
Chinese remainder theorem, specialized to two ideals.
Equations
- I.quotientInfEquivQuotientProd J coprime = (Ideal.quotEquivOfEq ⋯).trans ((Ideal.quotientInfRingEquivPiQuotient ![I, J] ⋯).trans (RingEquiv.piFinTwo fun (i : Fin 2) => R ⧸ ![I, J] i))
Chinese remainder theorem, specialized to two ideals.
Equations
- I.quotientMulEquivQuotientProd J coprime = (Ideal.quotEquivOfEq ⋯).trans (I.quotientInfEquivQuotientProd J coprime)
The R₁
-algebra structure on A/I
for an R₁
-algebra A
Equations
- Ideal.Quotient.algebra R₁ = Algebra.mk ((Ideal.Quotient.mk I).comp (algebraMap R₁ A)) ⋯ ⋯
Equations
- ⋯ = ⋯
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
- Ideal.Quotient.mkₐ R₁ I = { toFun := fun (a : A) => Submodule.Quotient.mk a, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
The canonical morphism A →ₐ[R₁] I.quotient
is surjective.
The kernel of A →ₐ[R₁] I.quotient
is I
.
Ideal.quotient.lift
as an AlgHom
.
Equations
- Ideal.Quotient.liftₐ I f hI = { toRingHom := Ideal.Quotient.lift I (↑f) hI, commutes' := ⋯ }
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
- Ideal.kerLiftAlg f = AlgHom.mk' (↑f).kerLift ⋯
The first isomorphism theorem for algebras, computable version.
Equations
- Ideal.quotientKerAlgEquivOfRightInverse hf = { toEquiv := (RingHom.quotientKerEquivOfRightInverse hf).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Alias of Ideal.quotientKerAlgEquivOfRightInverse_symm_apply
.
The first isomorphism theorem for algebras.
The ring hom R/I →+* S/J
induced by a ring hom f : R →+* S
with I ≤ f⁻¹(J)
Equations
- Ideal.quotientMap J f hIJ = Ideal.Quotient.lift I ((Ideal.Quotient.mk J).comp f) ⋯
The ring equiv R/I ≃+* S/J
induced by a ring equiv f : R ≃+* S
, where J = f(I)
.
Equations
- I.quotientEquiv J f hIJ = { toFun := (↑↑(Ideal.quotientMap J ↑f ⋯)).toFun, invFun := ⇑(Ideal.quotientMap I ↑f.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
H
and h
are kept as separate hypothesis since H is used in constructing the quotient map.
If we take J = I.comap f
then QuotientMap
is injective automatically.
Commutativity of a square is preserved when taking quotients by an ideal.
The algebra hom A/I →+* B/J
induced by an algebra hom f : A →ₐ[R₁] B
with I ≤ f⁻¹(J)
.
Equations
- Ideal.quotientMapₐ J f hIJ = { toRingHom := Ideal.quotientMap J (↑f) hIJ, commutes' := ⋯ }
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 = { toEquiv := (I.quotientEquiv J (↑f) hIJ).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Equations
- Ideal.quotientAlgebra = (Ideal.quotientMap I (algebraMap R A) ⋯).toAlgebra
Quotienting by equal ideals gives equivalent algebras.
Equations
- Ideal.quotientEquivAlgOfEq R₁ h = I.quotientEquivAlg J AlgEquiv.refl ⋯
The obvious ring hom R/I → R/(I ⊔ J)
Equations
- DoubleQuot.quotLeftToQuotSup I J = Ideal.Quotient.factor I (I ⊔ J) ⋯
The kernel of quotLeftToQuotSup
The ring homomorphism (R/I)/J' -> R/(I ⊔ J)
induced by quotLeftToQuotSup
where J'
is the image of J
in R/I
Equations
The composite of the maps R → (R/I)
and (R/I) → (R/I)/J'
Equations
- DoubleQuot.quotQuotMk I J = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk I)
The kernel of quotQuotMk
The ring homomorphism R/(I ⊔ J) → (R/I)/J'
induced by quotQuotMk
Equations
- DoubleQuot.liftSupQuotQuotMk I J = Ideal.Quotient.lift (I ⊔ J) (DoubleQuot.quotQuotMk I J) ⋯
quotQuotToQuotSup
and liftSupQuotQuotMk
are inverse isomorphisms. In the case where
I ≤ J
, this is the Third Isomorphism Theorem (see quotQuotEquivQuotOfLe
)
Equations
The obvious isomorphism (R/I)/J' → (R/J)/I'
Equations
- DoubleQuot.quotQuotEquivComm I J = ((DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯)).trans (DoubleQuot.quotQuotEquivQuotSup J I).symm
The Third Isomorphism theorem for rings. See quotQuotEquivQuotSup
for a version
that does not assume an inclusion of ideals.
Equations
- DoubleQuot.quotQuotEquivQuotOfLE h = (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯)
The natural algebra homomorphism A / I → A / (I ⊔ J)
.
Equations
- DoubleQuot.quotLeftToQuotSupₐ R I J = { toRingHom := DoubleQuot.quotLeftToQuotSup I J, commutes' := ⋯ }
The algebra homomorphism (A / I) / J' -> A / (I ⊔ J)
induced by quotQuotToQuotSup
,
where J'
is the projection of J
in A / I
.
Equations
- DoubleQuot.quotQuotToQuotSupₐ R I J = { toRingHom := DoubleQuot.quotQuotToQuotSup I J, commutes' := ⋯ }
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
- DoubleQuot.quotQuotMkₐ R I J = { toRingHom := DoubleQuot.quotQuotMk I J, commutes' := ⋯ }
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
- DoubleQuot.liftSupQuotQuotMkₐ R I J = { toRingHom := DoubleQuot.liftSupQuotQuotMk I J, commutes' := ⋯ }
quotQuotToQuotSup
and liftSupQuotQuotMk
are inverse isomorphisms. In the case where
I ≤ J
, this is the Third Isomorphism Theorem (see DoubleQuot.quotQuotEquivQuotOfLE
).
Equations
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
The third isomorphism theorem for algebras. See quotQuotEquivQuotSupₐ
for version
that does not assume an inclusion of ideals.
Equations
I ^ n ⧸ I ^ (n + 1)
can be viewed as a quotient module and as ideal of R ⧸ I ^ (n + 1)
.
This definition gives the R
-linear equivalence between the two.
Equations
- One or more equations did not get rendered due to their size.
I ^ n ⧸ I ^ (n + 1)
can be viewed as a quotient module and as ideal of R ⧸ I ^ (n + 1)
.
This definition gives the equivalence between the two, instead of the R
-linear equivalence,
to bypass typeclass synthesis issues on complex Module
goals.
Equations
- I.powQuotPowSuccEquivMapMkPowSuccPow n = ↑(I.powQuotPowSuccLinearEquivMapMkPowSuccPow n)