PhysLean 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
    • Ideal.comap f I = { 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} [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.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).)

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

                      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.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) :
                        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
                        • 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 : 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
                          • 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 : 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
                              def RingEquiv.idealComapOrderIso {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (e : R ≃+* S) :

                              Any ring isomorphism induces an order isomorphism of ideals.

                              Equations
                              Instances For
                                @[simp]
                                theorem RingEquiv.idealComapOrderIso_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (e : R ≃+* S) (I : Ideal S) :
                                @[simp]
                                theorem RingEquiv.idealComapOrderIso_symm_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (e : R ≃+* S) (I : Ideal R) :
                                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) :
                                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