The conductor ideal

This file defines the conductor ideal of an element x of R-algebra S. This is the ideal of S consisting of all elements a such that for all b in S, the product a * b lies in the R-subalgebra of S generated by x.

def conductor (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) : Ideal S

Let S / R be a ring extension and x : S, then the conductor of R<x> is the biggest ideal of S contained in R<x>.

Equations

• conductor R x = { carrier := {a : S | ∀ (b : S), a * b ∈ R[x]}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem conductor_eq_of_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x y : S} (h : ↑R[x] = ↑R[y]) : conductor R x = conductor R y

theorem conductor_subset_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} : ↑(conductor R x) ⊆ ↑R[x]

theorem mem_conductor_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x y : S} : y ∈ conductor R x ↔ ∀ (b : S), y * b ∈ R[x]

theorem conductor_eq_top_of_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} (h : R[x] = ⊤) : conductor R x = ⊤

theorem conductor_eq_top_of_powerBasis {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) : conductor R pb.gen = ⊤

theorem adjoin_eq_top_of_conductor_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} (h : conductor R x = ⊤) : R[x] = ⊤

theorem conductor_eq_top_iff_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} : conductor R x = ⊤ ↔ R[x] = ⊤

theorem mem_coeSubmodule_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {L : Type u_3} [CommRing L] [Algebra S L] [Algebra R L] [IsScalarTower R S L] [IsDomain S] [Module.IsTorsionFree S L] {x : S} {y : L} : y ∈ IsLocalization.coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ R[(algebraMap S L) x]

theorem prod_mem_ideal_map_of_mem_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} {p : R} {z : S} (hp : p ∈ Ideal.comap (algebraMap R S) (conductor R x)) (hz' : z ∈ Ideal.map (algebraMap R S) I) : (algebraMap R S) p * z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

This technical lemma tells us that if C is the conductor of R<x> and I is an ideal of R then p * (I * S) ⊆ I * R<x> for any p in C ∩ R

theorem comap_map_eq_map_adjoin_of_coprime_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)) : Ideal.comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I) = Ideal.map (algebraMap R ↥R[x]) I

A technical result telling us that (I * S) ∩ R<x> = I * R<x> for any ideal I of R.

noncomputable def quotAdjoinEquivQuotMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)) : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I ≃+* S ⧸ Ideal.map (algebraMap R S) I

The canonical morphism of rings from R<x> ⧸ (I*R<x>) to S ⧸ (I*S) is an isomorphism when I and (conductor R x) ∩ R are coprime.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem quotAdjoinEquivQuotMap_apply_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)) (a : ↥R[x]) : (quotAdjoinEquivQuotMap hx h_alg) ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥R[x]) I)) a) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ↑a

theorem Localization.localRingHom_bijective_of_not_conductor_le {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {P : Ideal S} [P.IsPrime] (hx : ¬conductor R x ≤ P) {s : Subalgebra R S} (hs : s = R[x]) (p : Ideal ↥s) [p.IsPrime] [P.LiesOver p] : Function.Bijective ⇑(localRingHom p P (algebraMap (↥s) S) ⋯)