More operations on modules and ideals #
Equations
- submodule.has_smul' = {smul := submodule.map₂ (linear_map.lsmul R M)}
This duplicates the global smul_eq_mul
, but doesn't have to unfold anywhere near as much to
apply.
N.annihilator
is the ideal of all elements r : R
such that r • N = 0
.
Equations
- N.annihilator = linear_map.ker (linear_map.lsmul R ↥N)
Given s
, a generating set of R
, to check that an x : M
falls in a
submodule M'
of x
, we only need to show that r ^ n • x ∈ M'
for some n
for each r : s
.
If x
is an I
-multiple of the submodule spanned by f '' s
,
then we can write x
as an I
-linear combination of the elements of f '' s
.
N.colon P
is the ideal of all elements r : R
such that r • P ⊆ N
.
Equations
- N.colon P = (submodule.map N.mkq P).annihilator
Equations
Equations
If I
divides J
, then I
contains J
.
In a Dedekind domain, to divide and contain are equivalent, see ideal.dvd_iff_le
.
Equations
- ideal.unique_units = {to_inhabited := {default := 1}, uniq := _}
I.comap f
is the preimage of I
under f
.
Instances for ideal.comap
The ideal
version of set.image_subset_preimage_of_inverse
.
The ideal
version of set.preimage_subset_image_of_inverse
.
The smallest S
-submodule that contains all x ∈ I * y ∈ J
is also the smallest R
-submodule that does so.
map
and comap
are adjoint, and the composition map f ∘ comap f
is the
identity
Equations
- ideal.gi_map_comap f hf = galois_insertion.monotone_intro _ _ _ _
Correspondence theorem
Equations
- ideal.rel_iso_of_surjective f hf = {to_equiv := {to_fun := λ (J : ideal S), ⟨ideal.comap f J, _⟩, inv_fun := λ (I : {p // ideal.comap f ⊥ ≤ p}), ideal.map f I.val, left_inv := _, right_inv := _}, map_rel_iff' := _}
The map on ideals induced by a surjective map preserves inclusion.
Equations
- ideal.order_embedding_of_surjective f hf = (rel_iso.to_rel_embedding (ideal.rel_iso_of_surjective f hf)).trans (subtype.rel_embedding has_le.le (λ (p : ideal R), ideal.comap f ⊥ ≤ p))
If f : R ≃+* S
is a ring isomorphism and I : ideal R
, then comap f.symm (comap f) = I
.
Special case of the correspondence theorem for isomorphic rings
Equations
- ideal.rel_iso_of_bijective f hf = {to_equiv := {to_fun := ideal.comap f, inv_fun := ideal.map f, left_inv := _, right_inv := _}, map_rel_iff' := _}
The pushforward ideal.map
as a monoid-with-zero homomorphism.
A proper ideal I
is primary iff xy ∈ I
implies x ∈ I
or y ∈ radical I
.
A variant of finsupp.total
that takes in vectors valued in I
.
Equations
- ideal.finsupp_total ι M I v = (finsupp.total ι M R v).comp (finsupp.map_range.linear_map (submodule.subtype I))
Kernel of a ring homomorphism as an ideal of the domain.
Equations
- ring_hom.ker f = ideal.comap f ⊥
An element is in the kernel if and only if it maps to zero.
If the target is not the zero ring, then one is not in the kernel.
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
- f.ker_lift = ideal.quotient.lift (ring_hom.ker f) f _
The induced map from the quotient by the kernel is injective.
The first isomorphism theorem for commutative rings, computable version.
Equations
- ring_hom.quotient_ker_equiv_of_right_inverse hf = {to_fun := ⇑(f.ker_lift), inv_fun := ⇑(ideal.quotient.mk (ring_hom.ker f)) ∘ g, left_inv := _, right_inv := hf, map_mul' := _, map_add' := _}
The first isomorphism theorem for commutative rings.
The kernel of a homomorphism to a domain is a prime ideal.
The kernel of a homomorphism to a field is a maximal ideal.
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 R₁
-algebra structure on A/I
for an R₁
-algebra A
Equations
- ideal.quotient.algebra R₁ = {to_has_smul := {smul := has_smul.smul (submodule.quotient.has_smul' I)}, to_ring_hom := {to_fun := λ (x : R₁), ⇑(ideal.quotient.mk I) (⇑(algebra_map R₁ A) x), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
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 = {to_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 alg_hom
.
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
The induced algebra morphism from the quotient by the kernel is injective.
The first isomorphism theorem for algebras, computable version.
Equations
- ideal.quotient_ker_alg_equiv_of_right_inverse hf = {to_fun := (ring_hom.quotient_ker_equiv_of_right_inverse _).to_fun, inv_fun := (ring_hom.quotient_ker_equiv_of_right_inverse _).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
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
- J.quotient_map f hIJ = ideal.quotient.lift I ((ideal.quotient.mk J).comp f) _
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 quotient_map
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)
.
The algebra equiv A/I ≃ₐ[R] B/J
induced by an algebra equiv f : A ≃ₐ[R] B
,
whereJ = f(I)
.
Equations
- ideal.quotient_algebra = (I.quotient_map (algebra_map R A) ideal.quotient_algebra._proof_1).to_algebra
Equations
- submodule.module_submodule = {to_distrib_mul_action := {to_mul_action := {to_has_smul := submodule.has_smul' _inst_3, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
Auxiliary definition used to define lift_of_right_inverse
lift_of_right_inverse f hf g hg
is the unique ring homomorphism φ
- such that
φ.comp f = g
(ring_hom.lift_of_right_inverse_comp
), - where
f : A →+* B
is has a right_inversef_inv
(hf
), - and
g : B →+* C
satisfieshg : f.ker ≤ g.ker
.
See ring_hom.eq_lift_of_right_inverse
for the uniqueness lemma.
A .
| \
f | \ g
| \
v \⌟
B ----> C
∃!φ
Equations
- f.lift_of_right_inverse f_inv hf = {to_fun := λ (g : {g // ring_hom.ker f ≤ ring_hom.ker g}), f.lift_of_right_inverse_aux f_inv hf g.val _, inv_fun := λ (φ : B →+* C), ⟨φ.comp f, _⟩, left_inv := _, right_inv := _}
A non-computable version of ring_hom.lift_of_right_inverse
for when no computable right
inverse is available, that uses function.surj_inv
.
The obvious ring hom R/I → R/(I ⊔ J)
Equations
- double_quot.quot_left_to_quot_sup I J = ideal.quotient.factor I (I ⊔ J) _
The kernel of quot_left_to_quot_sup
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
The composite of the maps R → (R/I)
and (R/I) → (R/I)/J'
Equations
- double_quot.quot_quot_mk I J = (ideal.quotient.mk (ideal.map (ideal.quotient.mk I) J)).comp (ideal.quotient.mk I)
The kernel of quot_quot_mk
The ring homomorphism R/(I ⊔ J) → (R/I)/J'
induced by quot_quot_mk
Equations
- double_quot.lift_sup_quot_quot_mk I J = ideal.quotient.lift (I ⊔ J) (double_quot.quot_quot_mk I J) _
quot_quot_to_quot_add
and lift_sup_double_qot_mk
are inverse isomorphisms
Equations
The obvious isomorphism (R/I)/J' → (R/J)/I'