Maps on modules and ideals #

Main definitions include Ideal.map, Ideal.comap, RingHom.ker, Module.annihilator and Submodule.annihilator.

def Ideal.map {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) :

Ideal S

I.map f is the span of the image of the ideal I under f, which may be bigger than the image itself.

Equations

Ideal.map f I = Ideal.span (⇑f '' ↑I)

Instances For

source

def Ideal.comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (I : Ideal S) :

Ideal R

I.comap f is the preimage of I under f.

Equations

Ideal.comap f I = { carrier := ⇑f ⁻¹' ↑I, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source

@[simp]

theorem Ideal.coe_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (I : Ideal S) :

↑(Ideal.comap f I) = ⇑f ⁻¹' ↑I

source

theorem Ideal.map_mono {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} {J : Ideal R} (h : I ≤ J) :

Ideal.map f I ≤ Ideal.map f J

source

theorem Ideal.mem_map_of_mem {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {I : Ideal R} {x : R} (h : x ∈ I) :

f x ∈ Ideal.map f I

source

theorem Ideal.apply_coe_mem_map {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) (x : ↥I) :

f ↑x ∈ Ideal.map f I

source

theorem Ideal.map_le_iff_le_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} {K : Ideal S} [RingHomClass F R S] :

Ideal.map f I ≤ K ↔ I ≤ Ideal.comap f K

source

@[simp]

theorem Ideal.mem_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {K : Ideal S} [RingHomClass F R S] {x : R} :

x ∈ Ideal.comap f K ↔ f x ∈ K

source

theorem Ideal.comap_mono {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {K : Ideal S} {L : Ideal S} [RingHomClass F R S] (h : K ≤ L) :

Ideal.comap f K ≤ Ideal.comap f L

source

theorem Ideal.comap_ne_top {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {K : Ideal S} [RingHomClass F R S] (hK : K ≠ ⊤) :

Ideal.comap f K ≠ ⊤

source

theorem Ideal.map_le_comap_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass G S R] (g : G) (I : Ideal R) (hf : Set.LeftInvOn ⇑g ⇑f ↑I) :

Ideal.map f I ≤ Ideal.comap g I

source

theorem Ideal.comap_le_map_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass F R S] (g : G) (I : Ideal S) (hf : Set.LeftInvOn (⇑g) (⇑f) (⇑f ⁻¹' ↑I)) :

Ideal.comap f I ≤ Ideal.map g I

source

theorem Ideal.map_le_comap_of_inverse {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass G S R] (g : G) (I : Ideal R) (h : Function.LeftInverse ⇑g ⇑f) :

Ideal.map f I ≤ Ideal.comap g I

The Ideal version of Set.image_subset_preimage_of_inverse.

source

theorem Ideal.comap_le_map_of_inverse {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass F R S] (g : G) (I : Ideal S) (h : Function.LeftInverse ⇑g ⇑f) :

Ideal.comap f I ≤ Ideal.map g I

The Ideal version of Set.preimage_subset_image_of_inverse.

source

instance Ideal.IsPrime.comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {K : Ideal S} [RingHomClass F R S] [hK : K.IsPrime] :

(Ideal.comap f K).IsPrime

Equations

⋯ = ⋯

source

theorem Ideal.map_top {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] :

Ideal.map f ⊤ = ⊤

source

theorem Ideal.gc_map_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] :

GaloisConnection (Ideal.map f) (Ideal.comap f)

source

@[simp]

theorem Ideal.comap_id {R : Type u} [Semiring R] (I : Ideal R) :

Ideal.comap (RingHom.id R) I = I

source

@[simp]

theorem Ideal.map_id {R : Type u} [Semiring R] (I : Ideal R) :

Ideal.map (RingHom.id R) I = I

source

theorem Ideal.comap_comap {R : Type u} {S : Type v} [Semiring R] [Semiring S] {T : Type u_3} [Semiring T] {I : Ideal T} (f : R →+* S) (g : S →+* T) :

Ideal.comap f (Ideal.comap g I) = Ideal.comap (g.comp f) I

source

theorem Ideal.comap_comapₐ {R : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] {I : Ideal C} (f : A →ₐ[R] B) (g : B →ₐ[R] C) :

Ideal.comap f (Ideal.comap g I) = Ideal.comap (g.comp f) I

source

theorem Ideal.map_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] {T : Type u_3} [Semiring T] {I : Ideal R} (f : R →+* S) (g : S →+* T) :

Ideal.map g (Ideal.map f I) = Ideal.map (g.comp f) I

source

theorem Ideal.map_mapₐ {R : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] {I : Ideal A} (f : A →ₐ[R] B) (g : B →ₐ[R] C) :

Ideal.map g (Ideal.map f I) = Ideal.map (g.comp f) I

source

theorem Ideal.map_span {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] (f : F) (s : Set R) :

Ideal.map f (Ideal.span s) = Ideal.span (⇑f '' s)

source

theorem Ideal.map_le_of_le_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} {K : Ideal S} [RingHomClass F R S] :

I ≤ Ideal.comap f K → Ideal.map f I ≤ K

source

theorem Ideal.le_comap_of_map_le {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} {K : Ideal S} [RingHomClass F R S] :

Ideal.map f I ≤ K → I ≤ Ideal.comap f K

source

theorem Ideal.le_comap_map {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} [RingHomClass F R S] :

I ≤ Ideal.comap f (Ideal.map f I)

source

theorem Ideal.map_comap_le {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {K : Ideal S} [RingHomClass F R S] :

Ideal.map f (Ideal.comap f K) ≤ K

source

@[simp]

theorem Ideal.comap_top {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} [RingHomClass F R S] :

Ideal.comap f ⊤ = ⊤

source

@[simp]

theorem Ideal.comap_eq_top_iff {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} [RingHomClass F R S] {I : Ideal S} :

Ideal.comap f I = ⊤ ↔ I = ⊤

source

@[simp]

theorem Ideal.map_bot {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} [RingHomClass F R S] :

Ideal.map f ⊥ = ⊥

source

theorem Ideal.ne_bot_of_map_ne_bot {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} [RingHomClass F R S] (hI : Ideal.map f I ≠ ⊥) :

I ≠ ⊥

source

@[simp]

theorem Ideal.map_comap_map {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) [RingHomClass F R S] :

Ideal.map f (Ideal.comap f (Ideal.map f I)) = Ideal.map f I

source

@[simp]

theorem Ideal.comap_map_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (K : Ideal S) [RingHomClass F R S] :

Ideal.comap f (Ideal.map f (Ideal.comap f K)) = Ideal.comap f K

source

theorem Ideal.map_sup {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) (J : Ideal R) [RingHomClass F R S] :

Ideal.map f (I ⊔ J) = Ideal.map f I ⊔ Ideal.map f J

source

theorem Ideal.comap_inf {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (K : Ideal S) (L : Ideal S) [RingHomClass F R S] :

Ideal.comap f (K ⊓ L) = Ideal.comap f K ⊓ Ideal.comap f L

source

theorem Ideal.map_iSup {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (K : ι → Ideal R) :

Ideal.map f (iSup K) = ⨆ (i : ι), Ideal.map f (K i)

source

theorem Ideal.comap_iInf {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (K : ι → Ideal S) :

Ideal.comap f (iInf K) = ⨅ (i : ι), Ideal.comap f (K i)

source

theorem Ideal.map_sSup {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (s : Set (Ideal R)) :

Ideal.map f (sSup s) = ⨆ I ∈ s, Ideal.map f I

source

theorem Ideal.comap_sInf {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (s : Set (Ideal S)) :

Ideal.comap f (sInf s) = ⨅ I ∈ s, Ideal.comap f I

source

theorem Ideal.comap_sInf' {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (s : Set (Ideal S)) :

Ideal.comap f (sInf s) = ⨅ I ∈ Ideal.comap f '' s, I

source

theorem Ideal.comap_isPrime {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (K : Ideal S) [RingHomClass F R S] [H : K.IsPrime] :

(Ideal.comap f K).IsPrime

Variant of Ideal.IsPrime.comap where ideal is explicit rather than implicit.

source

theorem Ideal.map_inf_le {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {I : Ideal R} {J : Ideal R} [RingHomClass F R S] :

Ideal.map f (I ⊓ J) ≤ Ideal.map f I ⊓ Ideal.map f J

source

theorem Ideal.le_comap_sup {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {K : Ideal S} {L : Ideal S} [RingHomClass F R S] :

Ideal.comap f K ⊔ Ideal.comap f L ≤ Ideal.comap f (K ⊔ L)

source

theorem element_smul_restrictScalars {R : Type u_4} {S : Type u_5} {M : Type u_6} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] (r : R) (N : Submodule S M) :

Submodule.restrictScalars R ((algebraMap R S) r • N) = r • Submodule.restrictScalars R N

source

theorem Ideal.smul_restrictScalars {R : Type u_4} {S : Type u_5} {M : Type u_6} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] (I : Ideal R) (N : Submodule S M) :

Submodule.restrictScalars R (Ideal.map (algebraMap R S) I • N) = I • Submodule.restrictScalars R N

source

@[simp]

theorem Ideal.smul_top_eq_map {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] (I : Ideal R) :

I • ⊤ = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)

source

@[simp]

theorem Ideal.coe_restrictScalars {R : Type u_4} {S : Type u_5} [CommSemiring R] [Semiring S] [Algebra R S] (I : Ideal S) :

↑(Submodule.restrictScalars R I) = ↑I

source

@[simp]

theorem Ideal.restrictScalars_mul {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] (I : Ideal S) (J : Ideal S) :

Submodule.restrictScalars R (I * J) = Submodule.restrictScalars R I * Submodule.restrictScalars R J

The smallest S-submodule that contains all x ∈ I * y ∈ J is also the smallest R-submodule that does so.

source

theorem Ideal.map_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) (I : Ideal S) :

Ideal.map f (Ideal.comap f I) = I

source

def Ideal.giMapComap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) :

GaloisInsertion (Ideal.map f) (Ideal.comap f)

map and comap are adjoint, and the composition map f ∘ comap f is the identity

Equations

Ideal.giMapComap f hf = GaloisInsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

Instances For

source

theorem Ideal.map_surjective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) :

Function.Surjective (Ideal.map f)

source

theorem Ideal.comap_injective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) :

Function.Injective (Ideal.comap f)

source

theorem Ideal.map_sup_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) (I : Ideal S) (J : Ideal S) :

Ideal.map f (Ideal.comap f I ⊔ Ideal.comap f J) = I ⊔ J

source

theorem Ideal.map_iSup_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (hf : Function.Surjective ⇑f) (K : ι → Ideal S) :

Ideal.map f (⨆ (i : ι), Ideal.comap f (K i)) = iSup K

source

theorem Ideal.map_inf_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) (I : Ideal S) (J : Ideal S) :

Ideal.map f (Ideal.comap f I ⊓ Ideal.comap f J) = I ⊓ J

source

theorem Ideal.map_iInf_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (hf : Function.Surjective ⇑f) (K : ι → Ideal S) :

Ideal.map f (⨅ (i : ι), Ideal.comap f (K i)) = iInf K

source

theorem Ideal.mem_image_of_mem_map_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) {I : Ideal R} {y : S} (H : y ∈ Ideal.map f I) :

y ∈ ⇑f '' ↑I

source

theorem Ideal.mem_map_iff_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) {I : Ideal R} {y : S} :

y ∈ Ideal.map f I ↔ ∃ x ∈ I, f x = y

source

theorem Ideal.le_map_of_comap_le_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {I : Ideal R} {K : Ideal S} [RingHomClass F R S] (hf : Function.Surjective ⇑f) :

Ideal.comap f K ≤ I → K ≤ Ideal.map f I

source

theorem Ideal.map_eq_submodule_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [h : RingHomSurjective f] (I : Ideal R) :

Ideal.map f I = Submodule.map f.toSemilinearMap I

source

theorem Ideal.comap_bot_le_of_injective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {I : Ideal R} [RingHomClass F R S] (hf : Function.Injective ⇑f) :

Ideal.comap f ⊥ ≤ I

source

theorem Ideal.comap_bot_of_injective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Injective ⇑f) :

Ideal.comap f ⊥ = ⊥

source

@[simp]

theorem Ideal.map_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (f : R ≃+* S) :

Ideal.map (↑f.symm) (Ideal.map (↑f) I) = I

If f : R ≃+* S is a ring isomorphism and I : Ideal R, then map f.symm (map f I) = I.

source

@[simp]

theorem Ideal.comap_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (f : R ≃+* S) :

Ideal.comap (↑f) (Ideal.comap (↑f.symm) I) = I

If f : R ≃+* S is a ring isomorphism and I : Ideal R, then comap f (comap f.symm I) = I.

source

theorem Ideal.map_comap_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (f : R ≃+* S) :

Ideal.map (↑f) I = Ideal.comap f.symm I

If f : R ≃+* S is a ring isomorphism and I : Ideal R, then map f I = comap f.symm I.

source

@[simp]

theorem Ideal.comap_symm {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (f : R ≃+* S) :

Ideal.comap f.symm I = Ideal.map f I

If f : R ≃+* S is a ring isomorphism and I : Ideal R, then comap f.symm I = map f I.

source

@[simp]

theorem Ideal.map_symm {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal S) (f : R ≃+* S) :

Ideal.map f.symm I = Ideal.comap f I

If f : R ≃+* S is a ring isomorphism and I : Ideal R, then map f.symm I = comap f I.

source

theorem Ideal.comap_map_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal R) :

Ideal.comap f (Ideal.map f I) = I ⊔ Ideal.comap f ⊥

source

def Ideal.relIsoOfSurjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) :

Ideal S ≃o { p : Ideal R // Ideal.comap f ⊥ ≤ p }

Correspondence theorem

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Ideal.orderEmbeddingOfSurjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) :

Ideal S ↪o Ideal R

The map on ideals induced by a surjective map preserves inclusion.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Ideal.map_eq_top_or_isMaximal_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) {I : Ideal R} (H : I.IsMaximal) :

Ideal.map f I = ⊤ ∨ (Ideal.map f I).IsMaximal

source

theorem Ideal.comap_isMaximal_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) {K : Ideal S} [H : K.IsMaximal] :

(Ideal.comap f K).IsMaximal

source

theorem Ideal.comap_le_comap_iff_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal S) (J : Ideal S) :

Ideal.comap f I ≤ Ideal.comap f J ↔ I ≤ J

source

def Ideal.relIsoOfBijective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Bijective ⇑f) :

Ideal S ≃o Ideal R

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' := ⋯ }

Instances For

source

theorem Ideal.comap_le_iff_le_map {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Bijective ⇑f) {I : Ideal R} {K : Ideal S} :

Ideal.comap f K ≤ I ↔ K ≤ Ideal.map f I

source

theorem Ideal.comap_map_of_bijective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Bijective ⇑f) {I : Ideal R} :

Ideal.comap f (Ideal.map f I) = I

source

theorem Ideal.map.isMaximal {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Bijective ⇑f) {I : Ideal R} (H : I.IsMaximal) :

(Ideal.map f I).IsMaximal

source

theorem Ideal.RingEquiv.bot_maximal_iff {R : Type u} {S : Type v} [Ring R] [Ring S] (e : R ≃+* S) :

⊥.IsMaximal ↔ ⊥.IsMaximal

source

theorem Ideal.map_mul {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) (J : Ideal R) :

Ideal.map f (I * J) = Ideal.map f I * Ideal.map f J

source

@[simp]

theorem Ideal.mapHom_apply {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) :

(Ideal.mapHom f) I = Ideal.map f I

source

def Ideal.mapHom {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) :

Ideal R →*₀ Ideal S

The pushforward Ideal.map as a monoid-with-zero homomorphism.

Equations

Ideal.mapHom f = { toFun := Ideal.map f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

theorem Ideal.map_pow {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) (n : ℕ) :

Ideal.map f (I ^ n) = Ideal.map f I ^ n

source

theorem Ideal.comap_radical {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (K : Ideal S) :

Ideal.comap f K.radical = (Ideal.comap f K).radical

source

theorem Ideal.IsRadical.comap {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : Ideal S} (hK : K.IsRadical) :

(Ideal.comap f K).IsRadical

source

theorem Ideal.map_radical_le {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {I : Ideal R} :

Ideal.map f I.radical ≤ (Ideal.map f I).radical

source

theorem Ideal.le_comap_mul {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : Ideal S} {L : Ideal S} :

Ideal.comap f K * Ideal.comap f L ≤ Ideal.comap f (K * L)

source

theorem Ideal.le_comap_pow {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : Ideal S} (n : ℕ) :

Ideal.comap f K ^ n ≤ Ideal.comap f (K ^ n)

source

def RingHom.ker {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) :

Ideal R

Kernel of a ring homomorphism as an ideal of the domain.

Equations

RingHom.ker f = Ideal.comap f ⊥

Instances For

source

@[simp]

theorem RingHom.mem_ker {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] {f : F} {r : R} :

r ∈ RingHom.ker f ↔ f r = 0

An element is in the kernel if and only if it maps to zero.

source

theorem RingHom.ker_eq {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) :

↑(RingHom.ker f) = ⇑f ⁻¹' {0}

source

theorem RingHom.ker_eq_comap_bot {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) :

RingHom.ker f = Ideal.comap f ⊥

source

theorem RingHom.comap_ker {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] [Semiring T] (f : S →+* R) (g : T →+* S) :

Ideal.comap g (RingHom.ker f) = RingHom.ker (f.comp g)

source

theorem RingHom.not_one_mem_ker {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] [Nontrivial S] (f : F) :

1 ∉ RingHom.ker f

If the target is not the zero ring, then one is not in the kernel.

source

theorem RingHom.ker_ne_top {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] [Nontrivial S] (f : F) :

RingHom.ker f ≠ ⊤

source

theorem Pi.ker_ringHom {S : Type v} [Semiring S] {ι : Type u_3} {R : ι → Type u_4} [(i : ι) → Semiring (R i)] (φ : (i : ι) → S →+* R i) :

RingHom.ker (Pi.ringHom φ) = ⨅ (i : ι), RingHom.ker (φ i)

source

@[simp]

theorem RingHom.ker_rangeSRestrict {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :

RingHom.ker f.rangeSRestrict = RingHom.ker f

source

theorem RingHom.injective_iff_ker_eq_bot {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) :

Function.Injective ⇑f ↔ RingHom.ker f = ⊥

source

theorem RingHom.ker_eq_bot_iff_eq_zero {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) :

RingHom.ker f = ⊥ ↔ ∀ (x : R), f x = 0 → x = 0

source

@[simp]

theorem RingHom.ker_coe_equiv {R : Type u} {S : Type v} [Ring R] [Semiring S] (f : R ≃+* S) :

RingHom.ker ↑f = ⊥

source

@[simp]

theorem RingHom.ker_equiv {R : Type u} {S : Type v} [Ring R] [Semiring S] {F' : Type u_2} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') :

RingHom.ker f = ⊥

source

theorem RingHom.sub_mem_ker_iff {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {x : R} {y : R} :

x - y ∈ RingHom.ker f ↔ f x = f y

source

@[simp]

theorem RingHom.ker_rangeRestrict {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) :

RingHom.ker f.rangeRestrict = RingHom.ker f

source

theorem RingHom.ker_isPrime {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [IsDomain S] [FunLike F R S] [RingHomClass F R S] (f : F) :

(RingHom.ker f).IsPrime

The kernel of a homomorphism to a domain is a prime ideal.

source

theorem RingHom.ker_isMaximal_of_surjective {R : Type u_1} {K : Type u_2} {F : Type u_3} [Ring R] [Field K] [FunLike F R K] [RingHomClass F R K] (f : F) (hf : Function.Surjective ⇑f) :

(RingHom.ker f).IsMaximal

The kernel of a homomorphism to a field is a maximal ideal.

source

def Module.annihilator (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :

Ideal R

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)

Instances For

source

theorem Module.mem_annihilator {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} :

r ∈ Module.annihilator R M ↔ ∀ (m : M), r • m = 0

source

theorem LinearMap.annihilator_le_of_injective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (hf : Function.Injective ⇑f) :

Module.annihilator R M' ≤ Module.annihilator R M

source

theorem LinearMap.annihilator_le_of_surjective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (hf : Function.Surjective ⇑f) :

Module.annihilator R M ≤ Module.annihilator R M'

source

theorem LinearEquiv.annihilator_eq {R : Type u_1} {M : Type u_2} {M' : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') :

Module.annihilator R M = Module.annihilator R M'

source

@[reducible, inline]

abbrev Submodule.annihilator {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :

Ideal R

N.annihilator is the ideal of all elements r : R such that r • N = 0.

Equations

N.annihilator = Module.annihilator R ↥N

Instances For

source

theorem Submodule.annihilator_top {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

⊤.annihilator = Module.annihilator R M

source

theorem Submodule.mem_annihilator {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {r : R} :

r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0

source

theorem Submodule.annihilator_bot {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

⊥.annihilator = ⊤

source

theorem Submodule.annihilator_eq_top_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :

N.annihilator = ⊤ ↔ N = ⊥

source

theorem Submodule.annihilator_mono {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {P : Submodule R M} (h : N ≤ P) :

P.annihilator ≤ N.annihilator

source

theorem Submodule.annihilator_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (ι : Sort w) (f : ι → Submodule R M) :

(⨆ (i : ι), f i).annihilator = ⨅ (i : ι), (f i).annihilator

source

theorem Submodule.mem_annihilator' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {r : R} :

r ∈ N.annihilator ↔ N ≤ Submodule.comap (r • LinearMap.id) ⊥

source

theorem Submodule.mem_annihilator_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set M) (r : R) :

r ∈ (Submodule.span R s).annihilator ↔ ∀ (n : ↑s), r • ↑n = 0

source

theorem Submodule.mem_annihilator_span_singleton {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (g : M) (r : R) :

r ∈ (Submodule.span R {g}).annihilator ↔ r • g = 0

source

@[simp]

theorem Submodule.annihilator_smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :

N.annihilator • N = ⊥

source

@[simp]

theorem Submodule.annihilator_mul {R : Type u_1} [CommSemiring R] (I : Ideal R) :

Submodule.annihilator I * I = ⊥

source

@[simp]

theorem Submodule.mul_annihilator {R : Type u_1} [CommSemiring R] (I : Ideal R) :

I * Submodule.annihilator I = ⊥

source

theorem Ideal.map_eq_bot_iff_le_ker {R : Type u_1} {S : Type u_2} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {I : Ideal R} (f : F) :

Ideal.map f I = ⊥ ↔ I ≤ RingHom.ker f

source

theorem Ideal.ker_le_comap {R : Type u_1} {S : Type u_2} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {K : Ideal S} (f : F) :

RingHom.ker f ≤ Ideal.comap f K

source

theorem Ideal.map_isPrime_of_equiv {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {F' : Type u_4} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') {I : Ideal R} [I.IsPrime] :

(Ideal.map f I).IsPrime

source

theorem Ideal.comap_map_of_surjective' {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal R) :

Ideal.comap f (Ideal.map f I) = I ⊔ RingHom.ker f

source

theorem Ideal.map_sInf {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] {A : Set (Ideal R)} {f : F} (hf : Function.Surjective ⇑f) :

(∀ J ∈ A, RingHom.ker f ≤ J) → Ideal.map f (sInf A) = sInf (Ideal.map f '' A)

source

theorem Ideal.map_isPrime_of_surjective {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} (hf : Function.Surjective ⇑f) {I : Ideal R} [H : I.IsPrime] (hk : RingHom.ker f ≤ I) :

(Ideal.map f I).IsPrime

source

theorem Ideal.map_eq_bot_iff_of_injective {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] {I : Ideal R} {f : F} (hf : Function.Injective ⇑f) :

Ideal.map f I = ⊥ ↔ I = ⊥

source

theorem Ideal.map_eq_iff_sup_ker_eq_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {I : Ideal R} {J : Ideal R} (f : R →+* S) (hf : Function.Surjective ⇑f) :

Ideal.map f I = Ideal.map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f

source

theorem Ideal.map_radical_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) {I : Ideal R} (h : RingHom.ker f ≤ I) :

Ideal.map f I.radical = (Ideal.map f I).radical

source

def RingHom.liftOfRightInverseAux {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g) :

B →+* C

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' := ⋯ }

Instances For

source

@[simp]

theorem RingHom.liftOfRightInverseAux_comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g) (a : A) :

(f.liftOfRightInverseAux f_inv hf g hg) (f a) = g a

source

def RingHom.liftOfRightInverse {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) :

{ g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C)

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_inverse f_inv (hf),
and g : B →+* C satisfies hg : 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.

Instances For

source

@[reducible, inline]

noncomputable abbrev RingHom.liftOfSurjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (hf : Function.Surjective ⇑f) :

{ g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C)

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) ⋯

Instances For

source

theorem RingHom.liftOfRightInverse_comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g : A →+* C // RingHom.ker f ≤ RingHom.ker g }) (x : A) :

((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x

source

theorem RingHom.liftOfRightInverse_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g : A →+* C // RingHom.ker f ≤ RingHom.ker g }) :

((f.liftOfRightInverse f_inv hf) g).comp f = ↑g

source

theorem RingHom.eq_liftOfRightInverse {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g) (h : B →+* C) (hh : h.comp f = g) :

h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

source

theorem AlgHom.coe_ker {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

RingHom.ker f = RingHom.ker ↑f

source

theorem AlgHom.coe_ideal_map {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Ideal A) :

Ideal.map f I = Ideal.map (↑f) I

source

theorem AlgHom.comap_ker {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] (f : B →ₐ[R] C) (g : A →ₐ[R] B) :

Ideal.comap g (RingHom.ker f) = RingHom.ker (f.comp g)

source

@[simp]

theorem Algebra.idealMap_apply_coe {R : Type u_1} [CommSemiring R] (S : Type u_2) [Semiring S] [Algebra R S] (I : Ideal R) (c : ↥I) :

↑((Algebra.idealMap S I) c) = (algebraMap R S) ↑c

source

def Algebra.idealMap {R : Type u_1} [CommSemiring R] (S : Type u_2) [Semiring S] [Algebra R S] (I : Ideal R) :

↥I →ₗ[R] ↥(Ideal.map (algebraMap R S) I)

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 ⋯

Instances For

source

theorem NoZeroSMulDivisors.of_ker_algebraMap_eq_bot (R : Type u_1) (A : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [NoZeroDivisors A] (h : RingHom.ker (algebraMap R A) = ⊥) :

NoZeroSMulDivisors R A

source

theorem NoZeroSMulDivisors.ker_algebraMap_eq_bot (R : Type u_1) (A : Type u_2) [CommRing R] [Ring A] [Nontrivial A] [Algebra R A] [NoZeroSMulDivisors R A] :

RingHom.ker (algebraMap R A) = ⊥

source

theorem NoZeroSMulDivisors.iff_ker_algebraMap_eq_bot {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [IsDomain A] [Algebra R A] :

NoZeroSMulDivisors R A ↔ RingHom.ker (algebraMap R A) = ⊥

Documentation

Mathlib.RingTheory.Ideal.Maps

Maps on modules and ideals #