More operations on modules and ideals
Equations
- submodule.has_scalar' = {smul := λ (I : ideal R) (N : submodule R M), ⨆ (r : ↥I), submodule.map (r.val • linear_map.id) N}
N.annihilator
is the ideal of all elements r : R
such that r • N = 0
.
Equations
- N.annihilator = (linear_map.lsmul R ↥N).ker
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
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 comaximal.
Equations
- ideal.quotient_inf_to_pi_quotient f = ideal.quotient.lift (⨅ (i : ι), f i) (_.mpr (pi.ring_hom (λ (i : ι), ideal.quotient.mk (f i)))) _
Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT
Equations
- ideal.quotient_inf_ring_equiv_pi_quotient f hf = {to_fun := (equiv.of_bijective ⇑(ideal.quotient_inf_to_pi_quotient (λ (i : ι), f i)) _).to_fun, inv_fun := (equiv.of_bijective ⇑(ideal.quotient_inf_to_pi_quotient (λ (i : ι), f i)) _).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
Equations
Equations
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))
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' := _}
Kernel of a ring homomorphism as an ideal of the domain.
Equations
- f.ker = ideal.comap f ⊥
If the target is not the zero ring, then one is not in the kernel.
The kernel of a homomorphism to an integral domain is a prime ideal.
The ring hom R/J →+* S/I
induced by a ring hom f : R →+* S
with J ≤ f⁻¹(I)
Equations
- J.quotient_map f hIJ = ideal.quotient.lift I ((ideal.quotient.mk J).comp f) _
H
and h
are kept as seperate 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.
Equations
- ideal.quotient_algebra = (J.quotient_map (algebra_map R S) ideal.quotient_algebra._proof_1).to_algebra
Equations
- submodule.semimodule_submodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := submodule.has_scalar' _inst_3, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
lift_of_surjective f hf g hg
is the unique ring homomorphism φ
- such that
φ.comp f = g
(lift_of_surjective_comp
), - where
f : A →+* B
is surjective (hf
), - and
g : B →+* C
satisfieshg : f.ker ≤ g.ker
.
See lift_of_surjective_eq
for the uniqueness lemma.
A .
| \
f | \ g
| \
v \⌟
B ----> C
∃!φ
Equations
- f.lift_of_surjective hf g hg = {to_fun := λ (b : B), ⇑g (classical.some _), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}