# Maps on modules and ideals #

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

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

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

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

Equations
• = { carrier := f ⁻¹' I, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem Ideal.coe_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (I : ) :
(Ideal.comap f I) = f ⁻¹' I
theorem Ideal.map_mono {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} {I : } {J : } (h : I J) :
theorem Ideal.mem_map_of_mem {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {I : } {x : R} (h : x I) :
f x
theorem Ideal.apply_coe_mem_map {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) (I : ) (x : { x : R // x I }) :
f x
theorem Ideal.map_le_iff_le_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} {I : } {K : } [RingHomClass F R S] :
K I
@[simp]
theorem Ideal.mem_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} {K : } [RingHomClass F R S] {x : R} :
x f x K
theorem Ideal.comap_mono {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} {K : } {L : } [RingHomClass F R S] (h : K L) :
theorem Ideal.comap_ne_top {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {K : } [RingHomClass F R S] (hK : K ) :
theorem Ideal.map_le_comap_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass G S R] (g : G) (I : ) (hf : Set.LeftInvOn g f I) :
theorem Ideal.comap_le_map_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass F R S] (g : G) (I : ) (hf : Set.LeftInvOn (⇑g) (⇑f) (f ⁻¹' I)) :
theorem Ideal.map_le_comap_of_inverse {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass G S R] (g : G) (I : ) (h : ) :

The Ideal version of Set.image_subset_preimage_of_inverse.

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

The Ideal version of Set.preimage_subset_image_of_inverse.

instance Ideal.IsPrime.comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {K : } [RingHomClass F R S] [hK : K.IsPrime] :
(Ideal.comap f K).IsPrime
Equations
• =
theorem Ideal.map_top {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] :
theorem Ideal.gc_map_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] :
@[simp]
theorem Ideal.comap_id {R : Type u} [] (I : ) :
= I
@[simp]
theorem Ideal.map_id {R : Type u} [] (I : ) :
theorem Ideal.comap_comap {R : Type u} {S : Type v} [] [] {T : Type u_3} [] {I : } (f : R →+* S) (g : S →+* T) :
Ideal.comap f (Ideal.comap g I) = Ideal.comap (g.comp f) I
theorem Ideal.map_map {R : Type u} {S : Type v} [] [] {T : Type u_3} [] {I : } (f : R →+* S) (g : S →+* T) :
Ideal.map g (Ideal.map f I) = Ideal.map (g.comp f) I
theorem Ideal.map_span {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [RingHomClass F R S] (f : F) (s : Set R) :
theorem Ideal.map_le_of_le_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} {I : } {K : } [RingHomClass F R S] :
I K
theorem Ideal.le_comap_of_map_le {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} {I : } {K : } [RingHomClass F R S] :
KI
theorem Ideal.le_comap_map {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} {I : } [RingHomClass F R S] :
theorem Ideal.map_comap_le {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} {K : } [RingHomClass F R S] :
@[simp]
theorem Ideal.comap_top {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} [RingHomClass F R S] :
@[simp]
theorem Ideal.comap_eq_top_iff {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} [RingHomClass F R S] {I : } :
@[simp]
theorem Ideal.map_bot {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] {f : F} [RingHomClass F R S] :
@[simp]
theorem Ideal.map_comap_map {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) (I : ) [RingHomClass F R S] :
@[simp]
theorem Ideal.comap_map_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) (K : ) [RingHomClass F R S] :
theorem Ideal.map_sup {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) (I : ) (J : ) [RingHomClass F R S] :
Ideal.map f (I J) =
theorem Ideal.comap_inf {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) (K : ) (L : ) [RingHomClass F R S] :
Ideal.comap f (K L) =
theorem Ideal.map_iSup {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (K : ι) :
Ideal.map f (iSup K) = ⨆ (i : ι), Ideal.map f (K i)
theorem Ideal.comap_iInf {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (K : ι) :
Ideal.comap f (iInf K) = ⨅ (i : ι), Ideal.comap f (K i)
theorem Ideal.map_sSup {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (s : Set (Ideal R)) :
Ideal.map f (sSup s) = Is,
theorem Ideal.comap_sInf {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (s : Set (Ideal S)) :
Ideal.comap f (sInf s) = Is,
theorem Ideal.comap_sInf' {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (s : Set (Ideal S)) :
Ideal.comap f (sInf s) = I, I
theorem Ideal.comap_isPrime {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) (K : ) [RingHomClass F R S] [H : K.IsPrime] :
(Ideal.comap f K).IsPrime
theorem Ideal.map_inf_le {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {I : } {J : } [RingHomClass F R S] :
Ideal.map f (I J)
theorem Ideal.le_comap_sup {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {K : } {L : } [RingHomClass F R S] :
theorem element_smul_restrictScalars {R : Type u_4} {S : Type u_5} {M : Type u_6} [] [] [Algebra R S] [] [Module R M] [Module S M] [] (r : R) (N : ) :
theorem Ideal.smul_restrictScalars {R : Type u_4} {S : Type u_5} {M : Type u_6} [] [] [Algebra R S] [] [Module R M] [Module S M] [] (I : ) (N : ) :
@[simp]
theorem Ideal.smul_top_eq_map {R : Type u_4} {S : Type u_5} [] [] [Algebra R S] (I : ) :
@[simp]
theorem Ideal.coe_restrictScalars {R : Type u_4} {S : Type u_5} [] [] [Algebra R S] (I : ) :
= I
@[simp]
theorem Ideal.restrictScalars_mul {R : Type u_4} {S : Type u_5} [] [] [Algebra R S] (I : ) (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} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : ) (I : ) :
def Ideal.giMapComap {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : ) :

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

Equations
Instances For
theorem Ideal.map_surjective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : ) :
theorem Ideal.comap_injective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : ) :
theorem Ideal.map_sup_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : ) (I : ) (J : ) :
Ideal.map f ( ) = I J
theorem Ideal.map_iSup_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (hf : ) (K : ι) :
Ideal.map f (⨆ (i : ι), Ideal.comap f (K i)) = iSup K
theorem Ideal.map_inf_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : ) (I : ) (J : ) :
Ideal.map f ( ) = I J
theorem Ideal.map_iInf_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (hf : ) (K : ι) :
Ideal.map f (⨅ (i : ι), Ideal.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} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : ) {I : } {y : S} (H : y ) :
y f '' I
theorem Ideal.mem_map_iff_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : ) {I : } {y : S} :
y xI, f x = y
theorem Ideal.le_map_of_comap_le_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {I : } {K : } [RingHomClass F R S] (hf : ) :
IK
theorem Ideal.map_eq_submodule_map {R : Type u} {S : Type v} [] [] (f : R →+* S) [h : ] (I : ) :
= Submodule.map f.toSemilinearMap I
theorem Ideal.comap_bot_le_of_injective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) {I : } [RingHomClass F R S] (hf : ) :
I
theorem Ideal.comap_bot_of_injective {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : ) :
@[simp]
theorem Ideal.map_of_equiv {R : Type u} {S : Type v} [] [] (I : ) (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.

@[simp]
theorem Ideal.comap_of_equiv {R : Type u} {S : Type v} [] [] (I : ) (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.

theorem Ideal.map_comap_of_equiv {R : Type u} {S : Type v} [] [] (I : ) (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.

@[simp]
theorem Ideal.comap_symm {R : Type u} {S : Type v} [] [] (I : ) (f : R ≃+* S) :
Ideal.comap f.symm 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} [] [] (I : ) (f : R ≃+* S) :
Ideal.map f.symm I =

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

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 : ) (I : ) :
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 : ) :
≃o { p : // p }

Correspondence theorem

Equations
• One or more equations did not get rendered due to their size.
Instances For
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 : ) :

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
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 : ) {I : } (H : I.IsMaximal) :
= (Ideal.map f I).IsMaximal
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 : ) {K : } [H : K.IsMaximal] :
(Ideal.comap f K).IsMaximal
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 : ) (I : ) (J : ) :
I J
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 : ) :

Special case of the correspondence theorem for isomorphic rings

Equations
• = { toFun := , invFun := , left_inv := , right_inv := , map_rel_iff' := }
Instances For
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 : ) {I : } {K : } :
I K
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 : ) {I : } (H : I.IsMaximal) :
(Ideal.map f I).IsMaximal
theorem Ideal.RingEquiv.bot_maximal_iff {R : Type u} {S : Type v} [Ring R] [Ring S] (e : R ≃+* S) :
.IsMaximal .IsMaximal
theorem Ideal.map_mul {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : ) (J : ) :
Ideal.map f (I * J) = *
@[simp]
theorem Ideal.mapHom_apply {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : ) :
def Ideal.mapHom {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) :

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

Equations
• = { toFun := , map_zero' := , map_one' := , map_mul' := }
Instances For
theorem Ideal.map_pow {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : ) (n : ) :
Ideal.map f (I ^ n) = ^ n
theorem Ideal.comap_radical {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (K : ) :
theorem Ideal.IsRadical.comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : } (hK : K.IsRadical) :
theorem Ideal.map_radical_le {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {I : } :
theorem Ideal.le_comap_mul {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : } {L : } :
* Ideal.comap f (K * L)
theorem Ideal.le_comap_pow {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : } (n : ) :
^ n Ideal.comap f (K ^ n)
def RingHom.ker {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) :

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

Equations
Instances For
theorem RingHom.mem_ker {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) {r : R} :
r 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} [] [] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) :
(RingHom.ker f) = f ⁻¹' {0}
theorem RingHom.ker_eq_comap_bot {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) :
theorem RingHom.comap_ker {R : Type u} {S : Type v} {T : Type w} [] [] [] (f : S →+* R) (g : T →+* S) :
= RingHom.ker (f.comp g)
theorem RingHom.not_one_mem_ker {R : Type u} {S : Type v} {F : Type u_1} [] [] [FunLike F R S] [rcf : RingHomClass F R S] [] (f : F) :
1

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} [] [] [FunLike F R S] [rcf : RingHomClass F R S] [] (f : F) :
theorem Pi.ker_ringHom {S : Type v} [] {ι : Type u_3} {R : ιType u_4} [(i : ι) → Semiring (R i)] (φ : (i : ι) → S →+* R i) :
= ⨅ (i : ι), RingHom.ker (φ i)
@[simp]
theorem RingHom.ker_rangeSRestrict {R : Type u} {S : Type v} [] [] (f : R →+* S) :
RingHom.ker f.rangeSRestrict =
theorem RingHom.injective_iff_ker_eq_bot {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) :
theorem RingHom.ker_eq_bot_iff_eq_zero {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [] [FunLike F R S] [rc : RingHomClass F R S] (f : F) :
∀ (x : R), f x = 0x = 0
@[simp]
theorem RingHom.ker_coe_equiv {R : Type u} {S : Type v} [Ring R] [] (f : R ≃+* S) :
@[simp]
theorem RingHom.ker_equiv {R : Type u} {S : Type v} [Ring R] [] {F' : Type u_2} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') :
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 f x = f y
@[simp]
theorem RingHom.ker_rangeRestrict {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) :
RingHom.ker f.rangeRestrict =
theorem RingHom.ker_isPrime {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring 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.

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

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

theorem Ideal.map_eq_bot_iff_le_ker {R : Type u_1} {S : Type u_2} {F : Type u_3} [] [] [FunLike F R S] [rc : RingHomClass F R S] {I : } (f : F) :
= I
theorem Ideal.ker_le_comap {R : Type u_1} {S : Type u_2} {F : Type u_3} [] [] [FunLike F R S] [rc : RingHomClass F R S] {K : } (f : F) :
theorem Ideal.map_isPrime_of_equiv {R : Type u_1} {S : Type u_2} [] [] {F' : Type u_4} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') {I : } [I.IsPrime] :
(Ideal.map f I).IsPrime
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 : ) :
(∀ JA, J)Ideal.map f (sInf A) = sInf ( '' 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 : ) {I : } [H : I.IsPrime] (hk : I) :
(Ideal.map f I).IsPrime
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 : } {f : F} (hf : ) :
theorem Ideal.map_eq_iff_sup_ker_eq_of_surjective {R : Type u_1} {S : Type u_2} [] [] {I : } {J : } (f : R →+* S) (hf : ) :
= I = J
theorem Ideal.map_radical_of_surjective {R : Type u_1} {S : Type u_2} [] [] {f : R →+* S} (hf : ) {I : } (h : I) :
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 : BA) (hf : Function.RightInverse f_inv f) (g : A →+* C) (hg : ) :
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
@[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 : BA) (hf : Function.RightInverse f_inv f) (g : A →+* C) (hg : ) (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 : BA) (hf : Function.RightInverse f_inv f) :
{ g : A →+* C // } (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
@[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 : ) :
{ g : A →+* C // } (B →+* C)

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

Equations
Instances For
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 : BA) (hf : Function.RightInverse f_inv f) (g : { g : A →+* C // }) (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 : BA) (hf : Function.RightInverse f_inv f) (g : { g : A →+* C // }) :
((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 : BA) (hf : Function.RightInverse f_inv f) (g : A →+* C) (hg : ) (h : B →+* C) (hh : h.comp f = g) :
h = (f.liftOfRightInverse f_inv hf) g, hg
theorem AlgHom.coe_ker {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
theorem AlgHom.coe_ideal_map {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : ) :
= Ideal.map (↑f) I
@[simp]
theorem Algebra.idealMap_apply_coe {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) (c : { x : R // x I }) :
((Algebra.idealMap S I) c) = (algebraMap R S) c
def Algebra.idealMap {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) :
{ x : R // x I } →ₗ[R] { x : S // x Ideal.map (algebraMap R S) I }

The induced linear map from I to the span of I in an R-algebra S.

Equations
• = .restrict
Instances For