Documentation

Mathlib.RingTheory.Ideal.Maps

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

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} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (I : Ideal S) :

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

      Equations
        Instances For
          @[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 ) :
          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) :
          QI, 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] :
          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] :
          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] :
          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] :
          @[simp]
          theorem Ideal.comap_id {R : Type u} [Semiring R] (I : Ideal R) :
          @[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 Kmap 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 KI 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] :
          @[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] :
          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 ) :
          @[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 (IJ) = map f Imap 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 (KL) = comap f Kcomap 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.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) = Is, 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) = Is, 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) = Icomap 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] :

          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 (IJ) map f Imap 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 Kcomap f L comap f (KL)
          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) :
          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) :
          @[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) :
          @[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) :
          @[simp]

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

          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} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective 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) :
              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 Icomap f J) = IJ
              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 Icomap f J) = IJ
              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 xI, 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 IK 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) :
              @[instance 100]
              theorem Ideal.IsMaximal.comap_piEvalRingHom {ι : Type u_4} {R : ιType u_5} [(i : ι) → Semiring (R i)] {i : ι} {I : Ideal (R i)} (h : 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) :

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

              Equations
                Instances For
                  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.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) :
                  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) :
                  @[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 xI, 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) :

                  Special case of the correspondence theorem for isomorphic rings

                  Equations
                    Instances For
                      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} :
                      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} :
                      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} :

                      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] :

                      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] :

                      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) :
                      @[deprecated Ideal.IsMaximal.map_bijective (since := "2024-12-07")]
                      theorem Ideal.map.isMaximal {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.


                      Alias of the reverse direction of Ideal.isMaximal_map_iff_of_bijective.

                      @[deprecated Ideal.IsMaximal.comap_bijective (since := "2024-12-07")]
                      theorem Ideal.comap.isMaximal {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} :

                      Alias of the reverse direction of Ideal.isMaximal_comap_iff_of_bijective.


                      Alias of the reverse direction of Ideal.isMaximal_comap_iff_of_bijective.

                      @[deprecated Ideal.isMaximal_iff_of_bijective (since := "2024-12-07")]
                      theorem Ideal.RingEquiv.bot_maximal_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] (hf : Function.Bijective f) :

                      Alias of Ideal.isMaximal_iff_of_bijective.

                      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) = Icomap 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) :

                      Correspondence theorem

                      Equations
                        Instances For
                          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] :
                          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) :

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

                          Equations
                            Instances For
                              @[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) :
                              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) :
                              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} :
                              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] :
                              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.

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

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

                              Equations
                                Instances For
                                  @[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) :
                                  @[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) :
                                  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) :
                                  1ker f

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

                                  @[deprecated RingHom.one_notMem_ker (since := "2025-05-23")]
                                  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) :
                                  1ker f

                                  Alias of RingHom.one_notMem_ker.


                                  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) :
                                  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) :
                                  @[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') :
                                  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) :
                                  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) :
                                  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 = 0x = 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) :

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

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

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

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

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

                                  Equations
                                    Instances For
                                      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]
                                      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) :
                                      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) :
                                      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') :
                                      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] :
                                      theorem Module.annihilator_eq_bot {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] :
                                      @[reducible, inline]
                                      abbrev Submodule.annihilator {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :

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

                                      Equations
                                        Instances For
                                          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 nN, r n = 0
                                          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) :
                                          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} :
                                          @[simp]
                                          theorem Submodule.annihilator_smul {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :
                                          @[simp]
                                          theorem Submodule.annihilator_mul {R : Type u_1} [Semiring R] (I : Ideal R) :
                                          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} :
                                          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 (span 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.ker (LinearMap.toSpanSingleton R M g)
                                          @[simp]
                                          theorem Submodule.mul_annihilator {R : Type u_1} [CommSemiring R] (I : Ideal R) :
                                          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) :
                                          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) :
                                          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.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) = IRingHom.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) :
                                          (∀ JA, 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.map_ne_bot_of_ne_bot {R : Type u_1} [CommRing R] {S : Type u_4} [Ring S] [Nontrivial S] [Algebra R S] [NoZeroSMulDivisors R S] {I : Ideal R} (h : 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 IRingHom.ker f = JRingHom.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 : BA) (hf : Function.RightInverse f_inv f) (g : A →+* C) (hg : ker f ker g) :
                                          B →+* C

                                          Auxiliary definition used to define liftOfRightInverse

                                          Equations
                                            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 : 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 : BA) (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 φ

                                              See RingHom.eq_liftOfRightInverse for the uniqueness lemma.

                                                 A .
                                                 |  \
                                               f |   \ g
                                                 |    \
                                                 v     \⌟
                                                 B ----> C
                                                    ∃!φ
                                              
                                              Equations
                                                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 : 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.

                                                  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 // 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 : BA) (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 : BA) (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 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) :
                                                      @[deprecated AlgHom.ker_coe (since := "2025-02-24")]
                                                      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) :

                                                      Alias of AlgHom.ker_coe.

                                                      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) :
                                                      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
                                                        Instances For
                                                          @[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
                                                          @[deprecated FaithfulSMul.ker_algebraMap_eq_bot (since := "2025-01-31")]

                                                          Alias of FaithfulSMul.ker_algebraMap_eq_bot.

                                                          @[deprecated FaithfulSMul.ker_algebraMap_eq_bot (since := "2025-01-31")]

                                                          Alias of FaithfulSMul.ker_algebraMap_eq_bot.

                                                          @[deprecated FaithfulSMul.ker_algebraMap_eq_bot (since := "2025-01-31")]

                                                          Alias of FaithfulSMul.ker_algebraMap_eq_bot.