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
Instances For
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
Instances For
Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT
Equations
Instances For
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
.
The R₁
-algebra structure on A/I
for an R₁
-algebra A
Equations
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
Instances For
The canonical morphism A →ₐ[R₁] I.quotient
is surjective.
The kernel of A →ₐ[R₁] I.quotient
is I
.
AlgHom
version of Ideal.Quotient.factor
.
Equations
Instances For
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
The first isomorphism theorem for algebras, computable version.
Equations
Instances For
The first isomorphism theorem for algebras.
Equations
Instances For
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
Instances For
The algebra equiv A/I ≃ₐ[R] B/J
induced by an algebra equiv f : A ≃ₐ[R] B
,
whereJ = f(I)
.
Equations
Instances For
If P
lies over p
, then R / p
has a canonical map to A / P
.
Equations
Instances For
Equations
Quotienting by equal ideals gives equivalent algebras.
Equations
Instances For
The first isomorphism theorem for commutative algebras (AlgHom.range
version).
Equations
Instances For
RingEquiv.quotientBot
as an algebra isomorphism.
Equations
Instances For
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
Instances For
The composite of the maps R → (R/I)
and (R/I) → (R/I)/J'
Equations
Instances For
The kernel of quotQuotMk
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
The obvious isomorphism (R/I)/J' → (R/J)/I'
Equations
Instances For
The Third Isomorphism theorem for rings. See quotQuotEquivQuotSup
for a version
that does not assume an inclusion of ideals.
Equations
Instances For
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
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
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
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
The third isomorphism theorem for algebras. See quotQuotEquivQuotSupₐ
for version
that does not assume an inclusion of ideals.
Equations
Instances For
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
Instances For
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.