Operations on ideal quotients

If I ≤ J are ideals with I finitely generated, then J.spanFinrank is at most that of its image in R ⧸ I plus that of I (Ideal.spanFinrank_le_spanFinrank_map_add_spanFinrank). This is the generator-lifting step in the proof of Stacks Project, Lemma 10.106.7. The bound is ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Bounding/PrincipalQuotientRegular.lean, and generalizes its Pcf.spanFinrank_maximalIdeal_le_add_one_of_principal_kernel from a principal kernel and the maximal ideal of a local ring to any ideals I ≤ J with I finitely generated.

For a principal quotient, if the image of an ideal is generated by the images of a set, adjoining the kernel generator to lifts of those quotient generators recovers the original ideal.

In the principal quotient R ⧸ (1 - e), the image of e is 1 (TauCeti.Ideal.Quotient.mk_span_singleton_one_sub_self); when e is idempotent this quotient is the component of R cut out by e.

If R / I → B / IB is surjective, algebra maps from B to an algebra annihilated by I are unique. This quotient extensionality lemma is used to construct compatible residue maps. More generally, if R ⧸ I → S ⧸ J is surjective, every element of S is congruent modulo J to the image of an element of R (Ideal.exists_sub_mem_of_surjective_quotientMap).

An action of a monoid by ring automorphisms preserving a two-sided ideal I descends to an action on the quotient by I (MonoidHom.quotientRingAut), assembled from Mathlib's Ideal.quotientEquiv.

If every class modulo a maximal ideal m comes from f, then m.comap f is maximal (Ideal.isMaximal_comap_of_surjective_quotient_mk_comp).

For an element p of a commutative R-algebra B, the sequence B → B → B ⧸ (p), whose first map is multiplication by p, is exact (Ideal.exact_mulLeft_mkₐ_span_singleton).

A linear endomorphism commuting with multiplication by each element of a set s induces an endomorphism of the quotient by Ideal.span s (Ideal.exists_quotient_linearMap_of_map_mul).

theorem Ideal.span_insert_eq_of_quotient {R : Type u_1} [CommRing R] (I : Ideal R) {x : R} (hmem : x ∈ I) (s : Set R) (himage : span (⇑(Quotient.mk (span {x})) '' s) = map (Quotient.mk (span {x})) I) : span (insert x s) = I

If the image of an ideal in a principal quotient is generated by the images of a set, adjoining the kernel generator to that set generates the original ideal.

theorem Ideal.algHom_ext_of_surjective_algebraMap_quotient {R : Type u_1} [CommRing R] (I : Ideal R) (B : Type u_2) [CommRing B] [Algebra R B] (hB : Function.Surjective ⇑(algebraMap (R ⧸ I) (B ⧸ map (algebraMap R B) I))) {S : Type u_3} [Semiring S] [Algebra R S] (hI : I ≤ RingHom.ker (algebraMap R S)) (f g : B →ₐ[R] S) : f = g

If R / I → B / IB is surjective, algebra maps from B to an algebra annihilated by I are unique.

theorem Ideal.exists_sub_mem_of_surjective_quotientMap {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {I : Ideal R} {J : Ideal S} {f : R →+* S} {hIJ : I ≤ comap f J} (hf : Function.Surjective ⇑(quotientMap J f hIJ)) (s : S) : ∃ (r : R), s - f r ∈ J

If R ⧸ I → S ⧸ J is surjective, every element of S is congruent modulo J to the image of an element of R.

theorem Ideal.spanFinrank_le_spanFinrank_map_add_spanFinrank {R : Type u_1} [CommRing R] {I J : Ideal R} (hIJ : I ≤ J) (hI : I.FG) : Submodule.spanFinrank J ≤ Submodule.spanFinrank (map (Quotient.mk I) J) + Submodule.spanFinrank I

If I ≤ J are ideals with I finitely generated, then J.spanFinrank is at most the sum of the spanFinranks of its image in R ⧸ I and I. For finitely generated J, this bounds its number of generators; for non-finitely-generated J, J.spanFinrank is defined to be 0. This is the ideal form of Submodule.spanFinrank_le_spanFinrank_map_mkQ_add_spanFinrank.

theorem Ideal.isMaximal_comap_of_surjective_quotient_mk_comp {A : Type u_2} {S : Type u_3} {F : Type u_4} [Ring A] [CommRing S] [FunLike F A S] [RingHomClass F A S] (f : F) {m : Ideal S} [m.IsMaximal] (hf : Function.Surjective (⇑(Quotient.mk m) ∘ ⇑f)) : (comap f m).IsMaximal

If every class modulo a maximal ideal m is the image of an element under f, then m.comap f is maximal: it is the kernel of the surjection from the source onto the field S ⧸ m. Compare Ideal.comap_isMaximal_of_surjective, which asks f itself to be surjective.

theorem Ideal.exists_quotient_linearMap_of_map_mul {k : Type u_2} {A : Type u_3} [CommRing k] [CommRing A] [Algebra k A] {s : Set A} (T : A →ₗ[k] A) (hmul : ∀ f ∈ s, ∀ (x : A), T (f * x) = f * T x) : ∃ (Q : A ⧸ span s →ₗ[k] A ⧸ span s), ∀ (x : A), Q ((Quotient.mk (span s)) x) = (Quotient.mk (span s)) (T x)

A linear endomorphism commuting with multiplication by each element of a set s preserves the ideal spanned by s, so it induces a compatible endomorphism of the quotient by that ideal.

theorem Ideal.Quotient.linearCombination_mk_map_apply {R : Type u_1} [CommRing R] {S : Type u_2} {ι : Type u_3} [CommRing S] [Algebra R S] [Fintype ι] (I : Ideal R) (b : ι → S) (c : ι → R) : ((Fintype.linearCombination (R ⧸ I) fun (j : ι) => (mk (map (algebraMap R S) I)) (b j)) fun (j : ι) => (mk I) (c j)) = (mk (map (algebraMap R S) I)) (∑ j : ι, (algebraMap R S) (c j) * b j)

The linear combination, with coefficients in R ⧸ I, of the classes in S ⧸ IS of elements b j of S, evaluated at the classes of c j, is the class of ∑ j, c j * b j.

theorem Ideal.exact_mulLeft_mkₐ_span_singleton {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] (p : B) : Function.Exact ⇑(LinearMap.mulLeft R p) ⇑(Quotient.mkₐ R (span {p})).toLinearMap

For an element p of a commutative R-algebra B, the sequence B → B → B ⧸ (p), whose first map is multiplication by p, is exact.

def MonoidHom.quotientRingAut {H : Type u_1} [Monoid H] {A : Type u_2} [Ring A] (a : H →* RingAut A) (I : Ideal A) [I.IsTwoSided] (hI : ∀ (h : H), Ideal.map (↑(a h)) I = I) : H →* RingAut (A ⧸ I)

An action of a monoid H on a ring A by ring automorphisms that preserve a two-sided ideal I descends to an action on A ⧸ I: the element h acts by Ideal.quotientEquiv I I (a h), which sends the class of x to the class of a h x.

@[simp]

theorem MonoidHom.quotientRingAut_apply_mk {H : Type u_1} [Monoid H] {A : Type u_2} [Ring A] (a : H →* RingAut A) (I : Ideal A) [I.IsTwoSided] (hI : ∀ (h : H), Ideal.map (↑(a h)) I = I) (h : H) (x : A) : ((a.quotientRingAut I hI) h) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk I) ((a h) x)

@[simp]

theorem MonoidHom.quotientRingAut_symm_apply_mk {H : Type u_1} [Monoid H] {A : Type u_2} [Ring A] (a : H →* RingAut A) (I : Ideal A) [I.IsTwoSided] (hI : ∀ (h : H), Ideal.map (↑(a h)) I = I) (h : H) (x : A) : (RingEquiv.symm ((a.quotientRingAut I hI) h)) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk I) ((RingEquiv.symm (a h)) x)

@[simp]

theorem TauCeti.Ideal.Quotient.mk_span_singleton_one_sub_self {R : Type u_1} [CommRing R] (e : R) : (Ideal.Quotient.mk (Ideal.span {1 - e})) e = 1

In the principal quotient R ⧸ (1 - e), the image of e is 1.