Conductor ideal

DefinitionConductor ideal of a subalgebra#✓fully proved

Let \(R\) be a commutative semiring, \(S\) a commutative \(R\)-algebra and \(A\) an \(R\)-subalgebra of \(S\). The conductor ideal of \(A\) is the ideal of \(S\) consisting of all \(s \in S\) such that \(st \in A\) for every \(t \in S\); it is the largest ideal of \(S\) contained in \(A\).

def conductorIdeal (A : Subalgebra R S) : Ideal S where
  carrier := {s : S | ∀ t : S, s * t ∈ A}
  zero_mem' t := by simp
  add_mem' ha hb t := by simpa only [add_mul] using A.add_mem (ha t) (hb t)
  smul_mem' c a ha t := by
    simpa only [smul_eq_mul, mul_left_comm, mul_assoc] using ha (c * t)

Used by 12

Used byConductor of a monogenic subalgebra · Finiteness of an overring via its conductor · A finite overring has nonzero conductor · Preimage of a conductor ideal · The conductor ideal is the unit ideal only for the whole algebra · Monotonicity of the conductor ideal · The conductor ideal lies in the subalgebra · Conductor ideal of the whole algebra · A subalgebra of a field with nonzero conductor is finite · Finiteness of the integral closure via the conductor · Universal property of the conductor ideal · Membership in the conductor ideal

TheoremMembership in the conductor ideal#✓fully proved

Let \(R\) and \(S\) be commutative semirings with \(S\) an \(R\)-algebra, and let \(A\) be an \(R\)-subalgebra of \(S\). An element \(s \in S\) lies in the conductor ideal of \(A\) if and only if \(st \in A\) for every \(t \in S\).

theorem mem_conductorIdeal {A : Subalgebra R S} {s : S} :
    s ∈ A.conductorIdeal ↔ ∀ t : S, s * t ∈ A

Uses 1 · Used by 6

Statement usesConductor ideal of a subalgebra

Used byA finite overring has nonzero conductor · Preimage of a conductor ideal · Monotonicity of the conductor ideal · Conductor ideal of the whole algebra · A subalgebra of a field with nonzero conductor is finite · Universal property of the conductor ideal

TheoremUniversal property of the conductor ideal#✓fully proved

Let \(R\) and \(S\) be commutative semirings with \(S\) an \(R\)-algebra, let \(A\) be an \(R\)-subalgebra of \(S\), and let \(I\) be an ideal of \(S\). Then \(I\) is contained in the conductor ideal of \(A\) if and only if \(I\) is contained in \(A\).

theorem le_conductorIdeal_iff {A : Subalgebra R S} {I : Ideal S} :
    I ≤ A.conductorIdeal ↔ (I : Set S) ⊆ (A : Set S)

Uses 2 · Used by 2

Statement usesConductor ideal of a subalgebra

Proof usesMembership in the conductor ideal

Used byThe conductor ideal is the unit ideal only for the whole algebra · The conductor ideal lies in the subalgebra

TheoremThe conductor ideal lies in the subalgebra#✓fully proved

Let \(R\) be a commutative semiring, \(S\) a commutative \(R\)-algebra and \(A\) an \(R\)-subalgebra of \(S\). Then the conductor ideal of \(A\) is contained in \(A\).

theorem conductorIdeal_subset (A : Subalgebra R S) :
    (A.conductorIdeal : Set S) ⊆ (A : Set S)

Uses 2

Statement usesConductor ideal of a subalgebra

Proof usesUniversal property of the conductor ideal

TheoremMonotonicity of the conductor ideal#✓fully proved

Let \(R\) be a commutative semiring, \(S\) a commutative \(R\)-algebra and \(A \subseteq B\) two \(R\)-subalgebras of \(S\). Then the conductor ideal of \(A\) is contained in the conductor ideal of \(B\).

theorem conductorIdeal_mono {A B : Subalgebra R S} (h : A ≤ B) :
    A.conductorIdeal ≤ B.conductorIdeal

Uses 2

Statement usesConductor ideal of a subalgebra

Proof usesMembership in the conductor ideal

TheoremConductor ideal of the whole algebra#✓fully proved

Let \(R\) be a commutative semiring and \(S\) a commutative \(R\)-algebra. The conductor ideal of \(S\), viewed as an \(R\)-subalgebra of itself, is the unit ideal \(S\).

@[simp]
theorem conductorIdeal_top : (⊤ : Subalgebra R S).conductorIdeal = ⊤

Uses 2 · Used by 1

Statement usesConductor ideal of a subalgebra

Proof usesMembership in the conductor ideal

Used byThe conductor ideal is the unit ideal only for the whole algebra

TheoremThe conductor ideal is the unit ideal only for the whole algebra#✓fully proved

Let \(R\) be a commutative semiring, \(S\) a commutative \(R\)-algebra and \(A\) an \(R\)-subalgebra of \(S\). The conductor ideal of \(A\) is all of \(S\) if and only if \(A = S\).

theorem conductorIdeal_eq_top_iff {A : Subalgebra R S} :
    A.conductorIdeal = ⊤ ↔ A = ⊤

Uses 3

Statement usesConductor ideal of a subalgebra

Proof usesConductor ideal of the whole algebra · Universal property of the conductor ideal

TheoremPreimage of a conductor ideal#✓fully proved

Let \(R\) be a commutative semiring, \(S\) and \(T\) commutative \(R\)-algebras, \(f \colon S \to T\) a homomorphism of \(R\)-algebras and \(B\) an \(R\)-subalgebra of \(T\). Then the preimage under \(f\) of the conductor ideal of \(B\) is contained in the conductor ideal of the subalgebra \(f^{-1}(B)\) of \(S\).

theorem conductorIdeal_comap_le (f : S →ₐ[R] T) (B : Subalgebra R T) :
    (B.conductorIdeal).comap f.toRingHom ≤ (B.comap f).conductorIdeal

Uses 2

Statement usesConductor ideal of a subalgebra

Proof usesMembership in the conductor ideal

TheoremConductor of a monogenic subalgebra#✓fully proved

Let \(R\) be a commutative ring, \(S\) a commutative \(R\)-algebra and \(x \in S\). The conductor ideal of the subalgebra \(R[x]\) of \(S\) generated by \(x\) equals the conductor of \(x\), the ideal of all \(a \in S\) such that \(ab \in R[x]\) for every \(b \in S\).

theorem adjoin_conductorIdeal {R' S' : Type*} [CommRing R'] [CommRing S']
    [Algebra R' S'] (x : S') :
    (Algebra.adjoin R' ({x} : Set S')).conductorIdeal = conductor R' x

Uses 1

Statement usesConductor ideal of a subalgebra

TheoremA finite overring has nonzero conductor#✓fully proved

Let \(R\) be an integral domain with fraction field \(K\), and let \(T\) be an \(R\)-subalgebra of \(K\) that is finitely generated as an \(R\)-module. Then the conductor ideal of the image of \(R\) in \(T\) (the smallest \(R\)-subalgebra of \(T\)) is nonzero.

theorem conductorIdeal_bot_ne_bot_of_finite [Module.Finite R ↥T] :
    (⊥ : Subalgebra R ↥T).conductorIdeal ≠ ⊥

Uses 2 · Used by 1

Statement usesConductor ideal of a subalgebra

Proof usesMembership in the conductor ideal

Used byFiniteness of an overring via its conductor

TheoremA subalgebra of a field with nonzero conductor is finite#✓fully proved

Let \(R\) be a Noetherian commutative ring, \(K\) a field that is an \(R\)-algebra, and \(T\) an \(R\)-subalgebra of \(K\). If the conductor ideal of the image of \(R\) in \(T\) (the smallest \(R\)-subalgebra of \(T\)) is nonzero, then \(T\) is finitely generated as an \(R\)-module.

theorem finite_of_conductorIdeal_bot_ne_bot
    (h : (⊥ : Subalgebra R ↥T).conductorIdeal ≠ ⊥) : Module.Finite R ↥T

Uses 2 · Used by 1

Statement usesConductor ideal of a subalgebra

Proof usesMembership in the conductor ideal

Used byFiniteness of an overring via its conductor

TheoremFiniteness of an overring via its conductor#✓fully proved

Let \(R\) be a Noetherian integral domain with fraction field \(K\), and let \(T\) be an \(R\)-subalgebra of \(K\). Then the conductor ideal of the image of \(R\) in \(T\) (the smallest \(R\)-subalgebra of \(T\)) is nonzero if and only if \(T\) is finitely generated as an \(R\)-module.

theorem bot_conductorIdeal_ne_bot_iff :
    (⊥ : Subalgebra R ↥T).conductorIdeal ≠ ⊥ ↔ Module.Finite R ↥T

Uses 3 · Used by 1

Statement usesConductor ideal of a subalgebra

Proof usesA finite overring has nonzero conductor · A subalgebra of a field with nonzero conductor is finite

Used byFiniteness of the integral closure via the conductor

TheoremFiniteness of the integral closure via the conductor#✓fully proved

Let \(R\) be a Noetherian integral domain with fraction field \(K\), and let \(\overline{R}\) be the integral closure of \(R\) in \(K\), viewed as an \(R\)-algebra. The conductor ideal of the smallest \(R\)-subalgebra of \(\overline{R}\) (the image of \(R\)) is a nonzero ideal of \(\overline{R}\) if and only if \(\overline{R}\) is finitely generated as an \(R\)-module.

theorem integralClosure_bot_conductorIdeal_ne_bot_iff :
    (⊥ : Subalgebra R ↥(integralClosure R K)).conductorIdeal ≠ ⊥ ↔
      Module.Finite R ↥(integralClosure R K)

Uses 2

Statement usesConductor ideal of a subalgebra

Proof usesFiniteness of an overring via its conductor

DefinitionResidue-ring isomorphism away from a denominator-clearing ideal#✓fully proved

Let \(B\) be an algebra over \(O\), where \(O\) and \(B\) are commutative rings, with structure map \(\varphi : O \to B\). Let \(\mathfrak q\) be a maximal ideal of \(B\) and let \(\mathfrak c\) be an ideal of \(B\) with \(\mathfrak c \not\subseteq \mathfrak q\) such that for every \(x \in \mathfrak c\) and every \(b \in B\) there is \(o \in O\) with \(\varphi(o) = xb\). This is the ring isomorphism \(O / \varphi^{-1}(\mathfrak q) \to B / \mathfrak q\) induced by \(\varphi\), which sends the class of \(o \in O\) to the class of \(\varphi(o)\).

Ideal.quotient_coprime_residue_equiv · 21 lines

def quotient_coprime_residue_equiv (hc : ¬ c ≤ q)
    (hclear : ∀ x ∈ c, ∀ b : B, ∃ o : O, algebraMap O B o = x * b) :
    O ⧸ q.comap (algebraMap O B) ≃+* B ⧸ q := by
  refine RingEquiv.ofBijective (Ideal.quotientMap q (algebraMap O B) le_rfl)
    ⟨Ideal.quotientMap_injective, ?_⟩
  obtain ⟨s, hs_mem, hs_notin⟩ := SetLike.not_le_iff_exists.mp hc
  obtain ⟨a₀, q₀, hq₀, ha₀⟩ := (inferInstance : q.IsMaximal).exists_inv hs_notin
  intro y
  obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective y
  obtain ⟨o, ho⟩ := hclear s hs_mem (b * a₀)
  refine ⟨Ideal.Quotient.mk _ o, ?_⟩
  simp only [Ideal.quotientMap_mk]
  rw [Ideal.Quotient.eq]
  have h1 : s * a₀ = 1 - q₀ := by linear_combination ha₀
  have hkey : algebraMap O B o - b = -(b * q₀) := by
    calc algebraMap O B o - b = s * (b * a₀) - b := by rw [ho]
      _ = b * (s * a₀) - b := by ring
      _ = b * (1 - q₀) - b := by rw [h1]
      _ = -(b * q₀) := by ring
  rw [hkey]
  exact q.neg_mem (q.mul_mem_left b hq₀)

Used by 3

Used byEqual ideal indices away from a denominator-clearing ideal · Equal cardinality of residue rings away from a denominator-clearing ideal · The residue-ring isomorphism on residue classes

TheoremThe residue-ring isomorphism on residue classes#✓fully proved

Let \(B\) be an algebra over \(O\), where \(O\) and \(B\) are commutative rings, with structure map \(\varphi : O \to B\). Let \(\mathfrak q\) be a maximal ideal of \(B\) and let \(\mathfrak c\) be an ideal of \(B\) with \(\mathfrak c \not\subseteq \mathfrak q\) such that for every \(x \in \mathfrak c\) and every \(b \in B\) there is \(o \in O\) with \(\varphi(o) = xb\). Then for every \(o \in O\), the residue-ring isomorphism \(O / \varphi^{-1}(\mathfrak q) \cong B / \mathfrak q\) sends the class of \(o\) to the class of \(\varphi(o)\).

@[simp]
theorem quotient_coprime_residue_equiv_apply_mk (hc : ¬ c ≤ q)
    (hclear : ∀ x ∈ c, ∀ b : B, ∃ o : O, algebraMap O B o = x * b) (o : O) :
    quotient_coprime_residue_equiv q c hc hclear (Ideal.Quotient.mk _ o) =
      Ideal.Quotient.mk _ (algebraMap O B o)

Uses 1

Statement usesResidue-ring isomorphism away from a denominator-clearing ideal

TheoremEqual cardinality of residue rings away from a denominator-clearing ideal#✓fully proved

Let \(B\) be an algebra over \(O\), where \(O\) and \(B\) are commutative rings, with structure map \(\varphi : O \to B\). Let \(\mathfrak q\) be a maximal ideal of \(B\) and let \(\mathfrak c\) be an ideal of \(B\) with \(\mathfrak c \not\subseteq \mathfrak q\) such that for every \(x \in \mathfrak c\) and every \(b \in B\) there is \(o \in O\) with \(\varphi(o) = xb\). Then \(O / \varphi^{-1}(\mathfrak q)\) and \(B / \mathfrak q\) have the same cardinality, where the cardinality of an infinite set is taken to be \(0\).

theorem nat_card_quotient_coprime_residue_eq (hc : ¬ c ≤ q)
    (hclear : ∀ x ∈ c, ∀ b : B, ∃ o : O, algebraMap O B o = x * b) :
    Nat.card (O ⧸ q.comap (algebraMap O B)) = Nat.card (B ⧸ q)

Uses 1

Proof usesResidue-ring isomorphism away from a denominator-clearing ideal

TheoremEqual ideal indices away from a denominator-clearing ideal#✓fully proved

Let \(B\) be an algebra over \(O\), where \(O\) and \(B\) are commutative rings, with structure map \(\varphi : O \to B\). Let \(\mathfrak q\) be a maximal ideal of \(B\) and let \(\mathfrak c\) be an ideal of \(B\) with \(\mathfrak c \not\subseteq \mathfrak q\) such that for every \(x \in \mathfrak c\) and every \(b \in B\) there is \(o \in O\) with \(\varphi(o) = xb\). Then the index of \(\varphi^{-1}(\mathfrak q)\) in \(O\) equals the index of \(\mathfrak q\) in \(B\), where the index of an ideal is the number of elements of the quotient, taken to be \(0\) when the quotient is infinite.

theorem cardQuot_coprime_residue_eq (hc : ¬ c ≤ q)
    (hclear : ∀ x ∈ c, ∀ b : B, ∃ o : O, algebraMap O B o = x * b) :
    Submodule.cardQuot (q.comap (algebraMap O B) : Submodule O O) =
      Submodule.cardQuot (q : Submodule B B)

Uses 1

Proof usesResidue-ring isomorphism away from a denominator-clearing ideal

TheoremPrime ideals stay prime under denominator clearing#✓fully proved

Let \(O\) and \(B\) be commutative rings, let \(B\) be an \(O\)-algebra whose structure map \(f \colon O \to B\) is injective, let \(\mathfrak p\) be a prime ideal of \(O\), and let \(\mathfrak c\) be an ideal of \(O\) with \(\mathfrak c + \mathfrak p = O\) such that \(f(x)\,b\) lies in the image of \(f\) for every \(x \in \mathfrak c\) and every \(b \in B\). Then the ideal \(\mathfrak p B\) of \(B\) generated by \(f(\mathfrak p)\) is prime.

The proof shows that the canonical map \(O/\mathfrak p \to B/\mathfrak p B\) is a ring isomorphism and transfers the integral-domain property across it.

theorem isPrime_map_of_coprime_clearDenom (p c : Ideal O) (hp : p.IsPrime)
    (hinj : Function.Injective (algebraMap O B))
    (hclear : ∀ x ∈ c, ∀ b : B,
      algebraMap O B x * b ∈ Set.range (algebraMap O B))
    (hsup : c ⊔ p = ⊤) : (p.map (algebraMap O B)).IsPrime

Used by 3

Used byExtension after contraction fixes primes away from the conductor · Bijection of nonzero primes away from the conductor · Bijection of primes away from the conductor

TheoremMaximal ideals stay maximal under denominator clearing#✓fully proved

Let \(O\) and \(B\) be commutative rings, let \(B\) be an \(O\)-algebra whose structure map \(f \colon O \to B\) is injective, let \(\mathfrak p\) be a maximal ideal of \(O\), and let \(\mathfrak c\) be an ideal of \(O\) with \(\mathfrak c + \mathfrak p = O\) such that \(f(x)\,b\) lies in the image of \(f\) for every \(x \in \mathfrak c\) and every \(b \in B\). Then the ideal \(\mathfrak p B\) of \(B\) generated by \(f(\mathfrak p)\) is maximal.

The proof shows that the canonical map \(O/\mathfrak p \to B/\mathfrak p B\) is a ring isomorphism and transfers the field property across it.

theorem isMaximal_map_of_coprime_clearDenom (p c : Ideal O) (hp : p.IsMaximal)
    (hinj : Function.Injective (algebraMap O B))
    (hclear : ∀ x ∈ c, ∀ b : B,
      algebraMap O B x * b ∈ Set.range (algebraMap O B))
    (hsup : c ⊔ p = ⊤) : (p.map (algebraMap O B)).IsMaximal

Used by 1

Used byIn dimension at most one, nonzero primes extend to maximal ideals under denominator clearing

TheoremIn dimension at most one, nonzero primes extend to maximal ideals under denominator clearing#✓fully proved

In dimension at most one, nonzero primes extend to maximal ideals under denominator clearing. Let \(O\) and \(B\) be commutative rings such that every nonzero prime ideal of \(O\) is maximal, let \(B\) be an \(O\)-algebra whose structure map \(f \colon O \to B\) is injective, let \(\mathfrak p\) be a nonzero prime ideal of \(O\), and let \(\mathfrak c\) be an ideal of \(O\) with \(\mathfrak c + \mathfrak p = O\) such that \(f(x)\,b\) lies in the image of \(f\) for every \(x \in \mathfrak c\) and every \(b \in B\). Then the ideal of \(B\) generated by \(f(\mathfrak p)\) is maximal.

Here dimension at most one means that every nonzero prime ideal of \(O\) is maximal; for an integral domain \(O\) this is the condition that \(O\) has Krull dimension at most one.

theorem isMaximal_map_of_dimensionLEOne (p c : Ideal O) [Ring.DimensionLEOne O]
    (hp : p.IsPrime) (hne : p ≠ ⊥)
    (hinj : Function.Injective (algebraMap O B))
    (hclear : ∀ x ∈ c, ∀ b : B,
      algebraMap O B x * b ∈ Set.range (algebraMap O B))
    (hsup : c ⊔ p = ⊤) : (p.map (algebraMap O B)).IsMaximal

Uses 1

Proof usesMaximal ideals stay maximal under denominator clearing

LemmaContraction after extension fixes primes away from the conductor#✓fully proved

Contraction after extension is the identity on primes not containing 𝔠.

lemma comap_map_eq_of_not_le_conductor
    {O B : Type*} [CommRing O] [CommRing B] [Algebra O B]
    {𝔠 𝔭 : Ideal O}
    (hf : Function.Injective (algebraMap O B))
    (hclear : ∀ c ∈ 𝔠, ∀ b : B,
      algebraMap O B c * b ∈ Set.range (algebraMap O B))
    (h𝔭 : 𝔭.IsPrime) (h𝔭_nc : ¬ 𝔠 ≤ 𝔭) :
    Ideal.comap (algebraMap O B) (Ideal.map (algebraMap O B) 𝔭) = 𝔭

Used by 2

Used byBijection of nonzero primes away from the conductor · Bijection of primes away from the conductor

LemmaContraction of a nonzero ideal is nonzero#✓fully proved

Contraction of a nonzero ideal is nonzero when 𝔠 is nonzero: a nonzero element of 𝔠 clears a nonzero element of 𝔮 back to a nonzero element of the contraction.

lemma comap_ne_bot_of_ne_bot
    {O B : Type*} [CommRing O] [CommRing B] [IsDedekindDomain B] [Algebra O B]
    {𝔠 : Ideal O}
    (hf : Function.Injective (algebraMap O B))
    (hclear : ∀ c ∈ 𝔠, ∀ b : B,
      algebraMap O B c * b ∈ Set.range (algebraMap O B))
    (h𝔠_ne : 𝔠 ≠ ⊥)
    {𝔮 : Ideal B} (h𝔮_ne : 𝔮 ≠ ⊥) :
    Ideal.comap (algebraMap O B) 𝔮 ≠ ⊥

Used by 2

Used byExtension after contraction fixes primes away from the conductor · Bijection of nonzero primes away from the conductor

LemmaExtension after contraction fixes primes away from the conductor#✓fully proved

Extension after contraction is the identity on primes of B not containing 𝔠.map f, using that B has Krull dimension at most one.

lemma map_comap_eq_of_not_le_map_conductor
    {O B : Type*} [CommRing O] [CommRing B] [IsDedekindDomain B] [Algebra O B]
    {𝔠 : Ideal O}
    (hf : Function.Injective (algebraMap O B))
    (hclear : ∀ c ∈ 𝔠, ∀ b : B,
      algebraMap O B c * b ∈ Set.range (algebraMap O B))
    (h𝔠_ne : 𝔠 ≠ ⊥)
    (hsup : ∀ (𝔭 : Ideal O), 𝔭.IsPrime → 𝔭 ≠ ⊥ → ¬ 𝔠 ≤ 𝔭 → 𝔠 ⊔ 𝔭 = ⊤)
    {𝔮 : Ideal B} (h𝔮 : 𝔮.IsPrime) (h𝔮_ne : 𝔮 ≠ ⊥)
    (h𝔮_nc : ¬ 𝔠.map (algebraMap O B) ≤ 𝔮) :
    Ideal.map (algebraMap O B) (Ideal.comap (algebraMap O B) 𝔮) = 𝔮

Uses 2 · Used by 1

Proof usesContraction of a nonzero ideal is nonzero · Prime ideals stay prime under denominator clearing

Used byBijection of primes away from the conductor

DefinitionBijection of primes away from the conductor#✓fully proved

Contraction and extension give an equivalence between all primes of B not containing 𝔠.map (algebraMap O B) and all primes of O not containing 𝔠, including the zero prime on both sides. This restores the full spectra in ATLAS NumberTheoryI Corollary 6.27.

Ideal.primeEquivOfNotLeConductor · 33 lines

noncomputable def primeEquivOfNotLeConductor
    {O B : Type*} [CommRing O] [CommRing B] [IsDedekindDomain B] [Algebra O B]
    (hf : Function.Injective (algebraMap O B))
    (𝔠 : Ideal O) (h𝔠_ne : 𝔠 ≠ ⊥)
    (hclear : ∀ c ∈ 𝔠, ∀ b : B,
      algebraMap O B c * b ∈ Set.range (algebraMap O B))
    (hsup : ∀ (𝔭 : Ideal O), 𝔭.IsPrime → 𝔭 ≠ ⊥ → ¬ 𝔠 ≤ 𝔭 → 𝔠 ⊔ 𝔭 = ⊤) :
    {𝔮 : Ideal B // 𝔮.IsPrime ∧ ¬ (𝔠.map (algebraMap O B) ≤ 𝔮)} ≃
      {𝔭 : Ideal O // 𝔭.IsPrime ∧ ¬ 𝔠 ≤ 𝔭} := by
  classical
  exact
    { toFun := fun 𝔮 =>
        ⟨𝔮.1.comap (algebraMap O B), 𝔮.2.1.comap (algebraMap O B),
          fun h => 𝔮.2.2 (Ideal.map_le_of_le_comap h)⟩
      invFun := fun 𝔭 =>
        ⟨𝔭.1.map (algebraMap O B), (by
          by_cases h𝔭_bot : 𝔭.1 = ⊥
          · rw [h𝔭_bot, Ideal.map_bot]
            infer_instance
          · exact Ideal.isPrime_map_of_coprime_clearDenom _ _ 𝔭.2.1 hf hclear
              (hsup 𝔭.1 𝔭.2.1 h𝔭_bot 𝔭.2.2)), (by
          rw [Ideal.map_le_iff_le_comap,
            comap_map_eq_of_not_le_conductor hf hclear 𝔭.2.1 𝔭.2.2]
          exact 𝔭.2.2)⟩
      left_inv := fun 𝔮 => Subtype.ext (by
        change Ideal.map (algebraMap O B) (Ideal.comap (algebraMap O B) 𝔮.1) = 𝔮.1
        by_cases h𝔮_bot : 𝔮.1 = ⊥
        · rw [h𝔮_bot]
          exact Ideal.map_comap_bot (f := algebraMap O B)
        · exact map_comap_eq_of_not_le_map_conductor hf hclear h𝔠_ne hsup
            𝔮.2.1 h𝔮_bot 𝔮.2.2)
      right_inv := fun 𝔭 =>
        Subtype.ext (comap_map_eq_of_not_le_conductor hf hclear 𝔭.2.1 𝔭.2.2) }

Uses 3 · Used by 1

Statement usesContraction after extension fixes primes away from the conductor · Prime ideals stay prime under denominator clearing · Extension after contraction fixes primes away from the conductor

Used byBijection of nonzero primes away from the conductor

DefinitionBijection of nonzero primes away from the conductor#✓fully proved

Contraction and extension give an equivalence between the nonzero primes of B not containing 𝔠.map (algebraMap O B) and the nonzero primes of O not containing 𝔠. This is the restriction of Ideal.primeEquivOfNotLeConductor to nonzero prime ideals.

Ideal.primeEquivOfCoprimeConductor · 30 lines

noncomputable def primeEquivOfCoprimeConductor
    {O B : Type*} [CommRing O] [CommRing B] [IsDedekindDomain B] [Algebra O B]
    (hf : Function.Injective (algebraMap O B))
    (𝔠 : Ideal O) (h𝔠_ne : 𝔠 ≠ ⊥)
    (hclear : ∀ c ∈ 𝔠, ∀ b : B,
      algebraMap O B c * b ∈ Set.range (algebraMap O B))
    (hsup : ∀ (𝔭 : Ideal O), 𝔭.IsPrime → 𝔭 ≠ ⊥ → ¬ 𝔠 ≤ 𝔭 → 𝔠 ⊔ 𝔭 = ⊤) :
    {𝔮 : Ideal B // 𝔮.IsPrime ∧ 𝔮 ≠ ⊥ ∧ ¬ (𝔠.map (algebraMap O B) ≤ 𝔮)} ≃
      {𝔭 : Ideal O // 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ ∧ ¬ 𝔠 ≤ 𝔭} :=
  let e := primeEquivOfNotLeConductor hf 𝔠 h𝔠_ne hclear hsup
  { toFun := fun 𝔮 =>
      ⟨𝔮.1.comap (algebraMap O B), 𝔮.2.1.comap (algebraMap O B),
        comap_ne_bot_of_ne_bot hf hclear h𝔠_ne 𝔮.2.2.1,
        fun h => 𝔮.2.2.2 (Ideal.map_le_of_le_comap h)⟩
    invFun := fun 𝔭 =>
      ⟨𝔭.1.map (algebraMap O B),
        Ideal.isPrime_map_of_coprime_clearDenom _ _ 𝔭.2.1 hf hclear
          (hsup 𝔭.1 𝔭.2.1 𝔭.2.2.1 𝔭.2.2.2),
        by rw [Ne, Ideal.map_eq_bot_iff_of_injective hf]; exact 𝔭.2.2.1,
        (by
          rw [Ideal.map_le_iff_le_comap,
            comap_map_eq_of_not_le_conductor hf hclear 𝔭.2.1 𝔭.2.2.2]
          exact 𝔭.2.2.2)⟩
    left_inv := fun 𝔮 =>
      Subtype.ext (congrArg
        (fun (𝔮 : {𝔮 : Ideal B // 𝔮.IsPrime ∧ ¬ 𝔠.map (algebraMap O B) ≤ 𝔮}) => 𝔮.1)
        (e.symm_apply_apply ⟨𝔮.1, 𝔮.2.1, 𝔮.2.2.2⟩))
    right_inv := fun 𝔭 =>
      Subtype.ext (congrArg (fun (𝔭 : {𝔭 : Ideal O // 𝔭.IsPrime ∧ ¬ 𝔠 ≤ 𝔭}) => 𝔭.1)
        (e.apply_symm_apply ⟨𝔭.1, 𝔭.2.1, 𝔭.2.2.2⟩)) }

Uses 4

Statement usesContraction after extension fixes primes away from the conductor · Contraction of a nonzero ideal is nonzero · Prime ideals stay prime under denominator clearing · Bijection of primes away from the conductor

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.