Maps on modules and ideals #
Main definitions include Ideal.map
, Ideal.comap
, RingHom.ker
, Module.annihilator
and Submodule.annihilator
.
I.comap f
is the preimage of I
under f
.
Equations
- Ideal.comap f I = { carrier := ⇑f ⁻¹' ↑I, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
The Ideal
version of Set.image_subset_preimage_of_inverse
.
The Ideal
version of Set.preimage_subset_image_of_inverse
.
Equations
- ⋯ = ⋯
Variant of Ideal.IsPrime.comap
where ideal is explicit rather than implicit.
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.giMapComap f hf = GaloisInsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯
If f : R ≃+* S
is a ring isomorphism and I : Ideal R
,
then comap f (comap f.symm I) = I
.
Correspondence theorem
Equations
- One or more equations did not get rendered due to their size.
The map on ideals induced by a surjective map preserves inclusion.
Equations
- One or more equations did not get rendered due to their size.
The pullback of a maximal ideal under a ring isomorphism is a maximal ideal.
Equations
- ⋯ = ⋯
Special case of the correspondence theorem for isomorphic rings
Equations
- Ideal.relIsoOfBijective f hf = { toFun := Ideal.comap f, invFun := Ideal.map f, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
The pushforward Ideal.map
as a monoid-with-zero homomorphism.
Equations
- Ideal.mapHom f = { toFun := Ideal.map f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
Kernel of a ring homomorphism as an ideal of the domain.
Equations
- RingHom.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 kernel of a homomorphism to a domain is a prime ideal.
The kernel of a homomorphism to a field is a maximal ideal.
Module.annihilator R M
is the ideal of all elements r : R
such that r • M = 0
.
Equations
- Module.annihilator R M = RingHom.ker (Module.toAddMonoidEnd R M)
N.annihilator
is the ideal of all elements r : R
such that r • N = 0
.
Equations
- N.annihilator = Module.annihilator R ↥N
Auxiliary definition used to define liftOfRightInverse
Equations
- f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun (b : B) => g (f_inv b), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
liftOfRightInverse f hf g hg
is the unique ring homomorphism φ
- such that
φ.comp f = g
(RingHom.liftOfRightInverse_comp
), - where
f : A →+* B
has a right_inversef_inv
(hf
), - and
g : B →+* C
satisfieshg : f.ker ≤ g.ker
.
See RingHom.eq_liftOfRightInverse
for the uniqueness lemma.
A .
| \
f | \ g
| \
v \⌟
B ----> C
∃!φ
Equations
- One or more equations did not get rendered due to their size.
A non-computable version of RingHom.liftOfRightInverse
for when no computable right
inverse is available, that uses Function.surjInv
.
Equations
- f.liftOfSurjective hf = f.liftOfRightInverse (Function.surjInv hf) ⋯
The induced linear map from I
to the span of I
in an R
-algebra S
.
Equations
- Algebra.idealMap S I = (Algebra.linearMap R S).restrict ⋯