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.

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.

@[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) : ↑(comap f I) = ⇑f ⁻¹' ↑I

theorem Ideal.comap_coe {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) : comap (↑f) I = comap f I

theorem Ideal.map_coe {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 R) : map (↑f) I = map f I

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 J : Ideal R} (h : I ≤ J) : map f I ≤ map f J

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 ∈ map f I

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 ∈ map f I

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] : map f I ≤ K ↔ I ≤ comap f K

@[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 ∈ comap f K ↔ f x ∈ K

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 L : Ideal S} [RingHomClass F R S] (h : K ≤ L) : comap f K ≤ comap f L

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 ≠ ⊤) : comap f K ≠ ⊤

theorem Ideal.exists_ideal_comap_le_prime {R : Type u} {F : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] [FunLike F R S] [RingHomClass F R S] {f : F} (P : Ideal R) [P.IsPrime] (I : Ideal S) (le : comap f I ≤ P) : ∃ Q ≥ I, Q.IsPrime ∧ comap f Q ≤ P

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) : map f I ≤ comap g I

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)) : comap f I ≤ map g I

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) : map f I ≤ comap g I

The Ideal version of Set.image_subset_preimage_of_inverse.

@[instance 100]

instance Ideal.instIsTwoSidedComap {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] [K.IsTwoSided] : (comap f K).IsTwoSided

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) : comap f I ≤ map g I

The Ideal version of Set.preimage_subset_image_of_inverse.

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

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] : map f ⊤ = ⊤

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 (map f) (comap f)

@[simp]

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

@[simp]

theorem Ideal.comap_idₐ {R : Type u_3} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] (I : Ideal S) : comap (AlgHom.id R S) I = I

@[simp]

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

@[simp]

theorem Ideal.map_idₐ {R : Type u_3} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] (I : Ideal S) : map (AlgHom.id R S) I = I

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) : comap f (comap g I) = comap (g.comp f) I

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) : comap f (comap g I) = comap (g.comp f) I

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) : map g (map f I) = map (g.comp f) I

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) : map g (map f I) = map (g.comp f) I

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) : map f (span s) = span (⇑f '' s)

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 ≤ comap f K → map f I ≤ K

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] : map f I ≤ K → I ≤ comap f K

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 ≤ comap f (map f I)

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] : map f (comap f K) ≤ K

@[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] : comap f ⊤ = ⊤

@[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} : comap f I = ⊤ ↔ I = ⊤

@[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] : map f ⊥ = ⊥

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 : map f I ≠ ⊥) : I ≠ ⊥

@[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] : map f (comap f (map f I)) = map f I

@[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] : comap f (map f (comap f K)) = comap f K

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 J : Ideal R) [RingHomClass F R S] : map f (I ⊔ J) = map f I ⊔ map f J

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 L : Ideal S) [RingHomClass F R S] : comap f (K ⊓ L) = comap f K ⊓ comap f L

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) : map f (iSup K) = ⨆ (i : ι), map f (K i)

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) : comap f (iInf K) = ⨅ (i : ι), comap f (K i)

theorem Ideal.comap_finsetInf {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Type u_4} (s : Finset ι) (K : ι → Ideal S) : comap f (s.inf K) = s.inf fun (i : ι) => comap f (K i)

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)) : map f (sSup s) = ⨆ I ∈ s, map f I

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)) : comap f (sInf s) = ⨅ I ∈ s, comap f I

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)) : comap f (sInf s) = ⨅ I ∈ comap f '' s, I

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] : (comap f K).IsPrime

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

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 J : Ideal R} [RingHomClass F R S] : map f (I ⊓ J) ≤ map f I ⊓ map f J

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 L : Ideal S} [RingHomClass F R S] : comap f K ⊔ comap f L ≤ comap f (K ⊔ L)

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

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 (map (algebraMap R S) I • N) = I • Submodule.restrictScalars R N

@[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 (map (algebraMap R S) I)

@[simp]

theorem Ideal.coe_restrictScalars {R : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] [IsScalarTower R S S] (I : Ideal S) : ↑(Submodule.restrictScalars R I) = ↑I

@[simp]

theorem Ideal.restrictScalars_mul {R : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] [IsScalarTower R S S] (I 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.

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) : map f (comap f I) = I

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 (map f) (comap f)

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

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 (map f)

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 (comap f)

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 J : Ideal S) : map f (comap f I ⊔ comap f J) = I ⊔ J

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) : map f (⨆ (i : ι), comap f (K i)) = iSup K

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 J : Ideal S) : map f (comap f I ⊓ comap f J) = I ⊓ J

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) : map f (⨅ (i : ι), comap f (K i)) = iInf K

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 ∈ map f I) : y ∈ ⇑f '' ↑I

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 ∈ map f I ↔ ∃ x ∈ I, f x = y

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) : comap f K ≤ I → K ≤ map f I

theorem Ideal.map_comap_eq_self_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] {E : Type u_4} [EquivLike E R S] [RingEquivClass E R S] (e : E) (I : Ideal S) : map e (comap e I) = I

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) : map f I = Submodule.map f.toSemilinearMap I

@[instance 100]

instance Ideal.instIsTwoSidedMapRingHomOfRingHomSurjective {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [RingHomSurjective f] (I : Ideal R) [I.IsTwoSided] : (map f I).IsTwoSided

theorem Ideal.IsMaximal.comap_piEvalRingHom {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → Semiring (R i)] {i : ι} {I : Ideal (R i)} (h : I.IsMaximal) : (comap (Pi.evalRingHom R i) I).IsMaximal

theorem Ideal.comap_le_comap_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 J : Ideal S) : comap f I ≤ comap f J ↔ I ≤ J

def Ideal.orderEmbeddingOfSurjective {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) : Ideal S ↪o Ideal R

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

theorem Ideal.map_eq_top_or_isMaximal_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} (H : I.IsMaximal) : map f I = ⊤ ∨ (map f I).IsMaximal

theorem Ideal.map_evalRingHom_pi {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → Semiring (R i)] {I : (i : ι) → Ideal (R i)} (i : ι) : map (Pi.evalRingHom R i) (pi I) = I i

def Ideal.piOrderIso {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → Semiring (R i)] [Finite ι] : Ideal ((i : ι) → R i) ≃o ((i : ι) → Ideal (R i))

Ideals in a finite direct product semiring Πᵢ Rᵢ are identified with tuples of ideals in the individual semirings, in an order-preserving way.

(Note that this is not in general true for infinite direct products: If infinitely many of the Rᵢ are nontrivial, then there exists an ideal of Πᵢ Rᵢ that is not of the form Πᵢ Iᵢ, namely the ideal of finitely supported elements of Πᵢ Rᵢ (it is also not a principal ideal).)

@[simp]

theorem Ideal.coe_piOrderIso_apply {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → Semiring (R i)] [Finite ι] (a✝ : Ideal ((i : ι) → R i)) (i : ι) : ↑(piOrderIso a✝ i) = ⋂ (s : Submodule (R i) (R i)), ⋂ (_ : ↑a✝ ⊆ (fun (a : (i : ι) → R i) => a i) ⁻¹' ↑s), ↑s

@[simp]

theorem Ideal.coe_piOrderIso_symm_apply {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → Semiring (R i)] [Finite ι] (a✝ : (i : ι) → Ideal (R i)) : ↑((RelIso.symm piOrderIso) a✝) = {r : (i : ι) → R i | ∀ (i : ι), r i ∈ a✝ i}

instance Ideal.instIsPrincipalIdealRingForallOfFinite {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → Semiring (R i)] [Finite ι] [∀ (i : ι), IsPrincipalIdealRing (R i)] : IsPrincipalIdealRing ((i : ι) → R i)

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) : comap f ⊥ ≤ I

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) : comap f ⊥ = ⊥

@[simp]

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

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

@[simp]

theorem Ideal.comap_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} (f : R ≃+* S) : comap (↑f) (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.

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem Ideal.symm_apply_mem_of_equiv_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} {f : R ≃+* S} {y : S} : f.symm y ∈ I ↔ y ∈ map f I

@[simp]

theorem Ideal.apply_mem_of_equiv_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} {f : R ≃+* S} {x : R} : f x ∈ map f I ↔ x ∈ I

theorem Ideal.mem_map_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] {E : Type u_4} [EquivLike E R S] [RingEquivClass E R S] (e : E) {I : Ideal R} (y : S) : y ∈ map e I ↔ ∃ x ∈ I, e x = y

def Ideal.relIsoOfBijective {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.Bijective ⇑f) : Ideal S ≃o Ideal R

Special case of the correspondence theorem for isomorphic rings

theorem Ideal.comap_le_iff_le_map {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.Bijective ⇑f) {I : Ideal R} {K : Ideal S} : comap f K ≤ I ↔ K ≤ map f I

theorem Ideal.comap_map_of_bijective {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.Bijective ⇑f) {I : Ideal R} : comap f (map f I) = I

theorem Ideal.isMaximal_map_iff_of_bijective {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.Bijective ⇑f) {I : Ideal R} : (map f I).IsMaximal ↔ I.IsMaximal

theorem Ideal.isMaximal_comap_iff_of_bijective {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.Bijective ⇑f) {K : Ideal S} : (comap f K).IsMaximal ↔ K.IsMaximal

theorem Ideal.IsMaximal.map_bijective {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.Bijective ⇑f) {I : Ideal R} : I.IsMaximal → (map f I).IsMaximal

Alias of the reverse direction of Ideal.isMaximal_map_iff_of_bijective.

theorem Ideal.IsMaximal.comap_bijective {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.Bijective ⇑f) {K : Ideal S} : K.IsMaximal → (comap f K).IsMaximal

Alias of the reverse direction of Ideal.isMaximal_comap_iff_of_bijective.

instance Ideal.map_isMaximal_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] {E : Type u_4} [EquivLike E R S] [RingEquivClass E R S] (e : E) {p : Ideal R} [hp : p.IsMaximal] : (map e p).IsMaximal

A ring isomorphism sends a maximal ideal to a maximal ideal.

instance Ideal.comap_isMaximal_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] {E : Type u_4} [EquivLike E R S] [RingEquivClass E R S] (e : E) {p : Ideal S} [hp : p.IsMaximal] : (comap e p).IsMaximal

The pullback of a maximal ideal under a ring isomorphism is a maximal ideal.

theorem Ideal.isMaximal_iff_of_bijective {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.Bijective ⇑f) : ⊥.IsMaximal ↔ ⊥.IsMaximal

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) : comap f (map f I) = I ⊔ comap f ⊥

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 // comap f ⊥ ≤ p }

Correspondence theorem

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] : (comap f K).IsMaximal

theorem Ideal.map_mul {S : Type v} {F : Type u_1} [CommSemiring S] {R : Type u_2} [Semiring R] [FunLike F R S] [RingHomClass F R S] (f : F) (I J : Ideal R) : map f (I * J) = map f I * map f J

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

The pushforward Ideal.map as a (semi)ring homomorphism.

@[simp]

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

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

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

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

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

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

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

theorem Ideal.disjoint_map_primeCompl_iff_comap_le {R : Type u} [CommSemiring R] {S : Type u_2} [Semiring S] {f : R →+* S} {p : Ideal R} {I : Ideal S} [p.IsPrime] : Disjoint ↑I ↑(Submonoid.map f p.primeCompl) ↔ comap f I ≤ p

theorem Ideal.comap_map_eq_self_iff_of_isPrime {R : Type u} [CommSemiring R] {S : Type u_2} [CommSemiring S] {f : R →+* S} (p : Ideal R) [p.IsPrime] : comap f (map f p) = p ↔ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p

For a prime ideal p of R, p extended to S and restricted back to R is p if and only if p is the restriction of a prime in S.

theorem Ideal.comap_map_eq_self_of_isMaximal {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) {p : Ideal R} [hP' : p.IsMaximal] (hP : map f p ≠ ⊤) : comap f (map f p) = p

For a maximal ideal p of R, p extended to S and restricted back to R is p if its image in S is not equal to ⊤.

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.

@[instance 100]

instance RingHom.instIsTwoSidedKer {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) : (ker f).IsTwoSided

@[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 ∈ ker f ↔ f r = 0

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

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) : ↑(ker f) = ⇑f ⁻¹' {0}

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) : ker f = Ideal.comap f ⊥

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 (ker f) = ker (f.comp g)

theorem RingHom.one_notMem_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 ∉ ker f

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

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) : ker f ≠ ⊤

theorem RingHom.ker_eq_top_of_subsingleton {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] [Subsingleton S] (f : F) : ker f = ⊤

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)

@[simp]

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

@[simp]

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

theorem RingHom.ker_coe_toRingHom {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) : ker ↑f = ker f

@[simp]

theorem RingHom.ker_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] {F' : Type u_3} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') : ker f = ⊥

theorem RingHom.ker_equiv_comp {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (e : S ≃+* T) : ker (e.toRingHom.comp f) = ker f

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 ↔ ker f = ⊥

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) : ker f = ⊥ ↔ ∀ (x : R), f x = 0 → x = 0

theorem RingHom.ker_comp_of_injective {R : Type u} {S : Type v} {T : Type w} [Ring R] [Semiring S] [Semiring T] (g : T →+* R) {f : R →+* S} (hf : Function.Injective ⇑f) : ker (f.comp g) = ker g

@[simp]

theorem AlgHom.ker_coe_equiv {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) : RingHom.ker ↑e = ⊥

Synonym for RingHom.ker_coe_equiv, but given an algebra equivalence.

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 y : R} : x - y ∈ ker f ↔ f x = f y

@[simp]

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

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

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

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

The kernel of a homomorphism to a division ring is a maximal ideal.

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.

theorem Module.mem_annihilator {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} : r ∈ annihilator R M ↔ ∀ (m : M), r • m = 0

@[instance 100]

instance instIsTwoSidedAnnihilator {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : (Module.annihilator R M).IsTwoSided

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

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'

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'

theorem Module.comap_annihilator {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {R₀ : Type u_4} [CommSemiring R₀] [Module R₀ M] [Algebra R₀ R] [IsScalarTower R₀ R M] : Ideal.comap (algebraMap R₀ R) (annihilator R M) = annihilator R₀ M

theorem Module.annihilator_eq_bot {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] : annihilator R M = ⊥ ↔ FaithfulSMul R M

theorem Module.annihilator_eq_top_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : annihilator R M = ⊤ ↔ Subsingleton M

theorem Module.annihilator_prod {R : Type u_1} {M : Type u_2} {M' : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] : annihilator R (M × M') = annihilator R M ⊓ annihilator R M'

theorem Module.annihilator_finsupp {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} [Nonempty ι] : annihilator R (ι →₀ M) = annihilator R M

theorem Module.annihilator_dfinsupp {R : Type u_1} [Semiring R] {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] : annihilator R (Π₀ (i : ι), M i) = ⨅ (i : ι), annihilator R (M i)

theorem Module.annihilator_pi {R : Type u_1} [Semiring R] {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] : annihilator R ((i : ι) → M i) = ⨅ (i : ι), annihilator R (M i)

@[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.

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

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

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

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 = ⊥

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

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

theorem Submodule.le_annihilator_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {I : Ideal R} : I ≤ N.annihilator ↔ I • N = ⊥

@[simp]

theorem Submodule.annihilator_smul {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : N.annihilator • N = ⊥

@[simp]

theorem Submodule.annihilator_mul {R : Type u_1} [Semiring R] (I : Ideal R) : annihilator I * I = ⊥

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 ≤ comap (r • LinearMap.id) ⊥

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 ∈ (span R s).annihilator ↔ ∀ (n : ↑s), r • ↑n = 0

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 ∈ (R ∙ g).annihilator ↔ r • g = 0

theorem Submodule.annihilator_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set M) : (span R s).annihilator = ⨅ (g : ↑s), (LinearMap.toSpanSingleton R M ↑g).ker

theorem Submodule.annihilator_span_singleton {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (g : M) : (R ∙ g).annihilator = (LinearMap.toSpanSingleton R M g).ker

@[simp]

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

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) : map f I = ⊥ ↔ I ≤ RingHom.ker f

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 ≤ comap f K

instance 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] : (map f I).IsPrime

A ring isomorphism sends a prime ideal to a prime ideal.

theorem Ideal.map_eq_bot_iff_of_injective {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} (hf : Function.Injective ⇑f) : map f I = ⊥ ↔ I = ⊥

theorem Ideal.map_pointwise_smul {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (r : R) (I : Ideal R) (f : R →+* S) : map f (r • I) = f r • map f I

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) : comap f (map f I) = I ⊔ RingHom.ker f

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) → map f (sInf A) = sInf (map f '' A)

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) : (map f I).IsPrime

theorem Ideal.IsMaximal.map_of_surjective_of_ker_le {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) {m : Ideal R} [m.IsMaximal] (hk : RingHom.ker f ≤ m) : (map f m).IsMaximal

theorem Ideal.map_ne_bot_of_ne_bot {R : Type u_1} [CommRing R] [IsDomain R] {S : Type u_4} [Ring S] [Nontrivial S] [Algebra R S] [Module.IsTorsionFree R S] {I : Ideal R} (h : I ≠ ⊥) : map (algebraMap R S) I ≠ ⊥

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

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) : map f I.radical = (map f I).radical

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 : ker f ≤ ker g) : B →+* C

Auxiliary definition used to define liftOfRightInverse

@[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 : ker f ≤ ker g) (a : A) : (f.liftOfRightInverseAux f_inv hf g hg) (f a) = g a

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 // ker f ≤ 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
      ∃!φ

@[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 // ker f ≤ ker g } ≃ (B →+* C)

A non-computable version of RingHom.liftOfRightInverse for when no computable right inverse is available, that uses Function.surjInv.

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 // ker f ≤ ker g }) (x : A) : ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x

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 // ker f ≤ ker g }) : ((f.liftOfRightInverse f_inv hf) g).comp f = ↑g

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 : ker f ≤ ker g) (h : B →+* C) (hh : h.comp f = g) : h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

theorem RingHom.liftOfSurjective_comp_apply {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 : { g : A →+* C // ker f ≤ ker g }) (x : A) : ((f.liftOfSurjective hf) g) (f x) = ↑g x

theorem RingHom.liftOfSurjective_comp {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 : { g : A →+* C // ker f ≤ ker g }) : ((f.liftOfSurjective hf) g).comp f = ↑g

theorem RingHom.eq_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) (hg : ker f ≤ ker g) (h : B →+* C) (hh : h.comp f = g) : h = (f.liftOfSurjective hf) ⟨g, hg⟩

def RingEquiv.idealComapOrderIso {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (e : R ≃+* S) : Ideal S ≃o Ideal R

Any ring isomorphism induces an order isomorphism of ideals.

@[simp]

theorem RingEquiv.idealComapOrderIso_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (e : R ≃+* S) (I : Ideal S) : e.idealComapOrderIso I = Ideal.comap e I

@[simp]

theorem RingEquiv.idealComapOrderIso_symm_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (e : R ≃+* S) (I : Ideal R) : e.idealComapOrderIso.symm I = Ideal.map e I

theorem AlgHom.ker_coe {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

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

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)

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.

@[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) : ↑((idealMap S I) c) = (algebraMap R S) ↑c

@[simp]

theorem FaithfulSMul.ker_algebraMap_eq_bot (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] : RingHom.ker (algebraMap R A) = ⊥

instance instIsPrincipalMapRingHom {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (I : Ideal R) [Submodule.IsPrincipal I] : Submodule.IsPrincipal (Ideal.map f I)

theorem RingHom.ker_evalRingHom {ι : Type u_1} [DecidableEq ι] (R : ι → Type u_2) [(i : ι) → CommRing (R i)] (i : ι) : ker (Pi.evalRingHom R i) = Ideal.span {1 - Pi.single i 1}