def Subalgebra.conductorIdeal (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (A : Subalgebra R S) : Ideal S

class IsOrder (O : Type u_1) [CommRing O] [IsDomain O] : Prop

• isNoetherian : IsNoetherianRing O
• dimLEOne : Ring.DimensionLEOne O
• notIsField : ¬IsField O
• intClosureFG (K : Type u_2) [Field K] [Algebra O K] [IsFractionRing O K] : Module.Finite O ↥(integralClosure O K)

class IsAOrder (A : Type u_1) (L : Type u_2) [CommRing A] [CommRing L] [Algebra A L] (O : Subalgebra A L) : Prop

• fg : (Subalgebra.toSubmodule O).FG
• spans (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [Algebra K L] [IsScalarTower A K L] : Submodule.span K (Set.range Subtype.val) = ⊤

theorem conductor_ne_bot_of_fg_subalgebra {R : Type u_3} [CommRing R] [IsDomain R] {K : Type u_4} [Field K] [Algebra R K] [IsFractionRing R K] (S : Subalgebra R K) (hS : (Subalgebra.toSubmodule S).FG) : ∃ (d : R), d ≠ 0 ∧ ∀ s ∈ S, (algebraMap R K) d * s ∈ (algebraMap R K).range

theorem conductor_ne_bot_iff_module_finite {R : Type u_3} [CommRing R] [IsDomain R] [IsNoetherianRing R] {K : Type u_4} [Field K] [Algebra R K] [IsFractionRing R K] (S : Subalgebra R K) : (∃ (d : R), d ≠ 0 ∧ ∀ s ∈ S, (algebraMap R K) d * s ∈ (algebraMap R K).range) ↔ (Subalgebra.toSubmodule S).FG

theorem finite_primes_containing_ideal {B : Type u_1} [CommRing B] [IsDomain B] [IsDedekindDomain B] {𝔠 : Ideal B} (h𝔠 : 𝔠 ≠ ⊥) : {𝔭 : Ideal B | 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ ∧ 𝔠 ≤ 𝔭}.Finite

theorem order_prime_decomposition {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) : have e := KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx'; ∀ {J : Ideal S} (hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)), emultiplicity J (Ideal.map (algebraMap R S) I) = emultiplicity (↑(e ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))

theorem nonZeroDivisors_le_comap_atPrime {A : Type u_1} [CommRing A] (𝔭 : Ideal A) [𝔭.IsPrime] : nonZeroDivisors A ≤ Submonoid.comap (algebraMap A (Localization.AtPrime 𝔭)) (nonZeroDivisors (Localization.AtPrime 𝔭))

def FractionalIdeal.IsPrimeTo {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] (I : FractionalIdeal (nonZeroDivisors A) (Localization (nonZeroDivisors A))) (J : Ideal A) : Prop

def invertibleFractionalIdealsPrimeTo {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] (J : Ideal A) : Subgroup (FractionalIdeal (nonZeroDivisors A) (Localization (nonZeroDivisors A)))ˣ

class IsAOrder_AKLB (A : Type u_1) (L : Type u_2) [CommRing A] [IsDomain A] [IsNoetherianRing A] [CommRing L] [IsDomain L] [Algebra A L] (O : Subalgebra A L) : Prop

• fg : (Subalgebra.toSubmodule O).FG
• spans (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [Algebra K L] [IsScalarTower A K L] : Submodule.span K (Set.range Subtype.val) = ⊤

theorem order_iff_fg_integral {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [CommRing L] [IsDomain L] [Algebra A L] [Algebra K L] [Algebra B L] [IsScalarTower A K L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Module.Finite A B] (O : Subalgebra A L) [IsFractionRing (↥O) L] (hA : ¬IsField A) : IsAOrder_AKLB A L O ↔ IsOrder ↥O ∧ IsIntegralClosure B (↥O) L

theorem conductor_span_helper {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [Algebra O B] {𝔠 𝔭 : Ideal O} (h𝔠_cond : ∀ c ∈ 𝔠, ∀ (b : B), (algebraMap O B) c * b ∈ (algebraMap O B).range) {s : O} (hs𝔠 : s ∈ 𝔠) {x : B} (hx : x ∈ Ideal.map (algebraMap O B) 𝔭) : ∃ (n : ℕ), ∃ q ∈ 𝔭, (algebraMap O B) q = (algebraMap O B) s ^ n * x

theorem ideal_extension_prime_coprime_conductor {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra O B] (hf : Function.Injective ⇑(algebraMap O B)) {𝔠 𝔭 : Ideal O} [h𝔭 : 𝔭.IsPrime] (h𝔠_cond : ∀ c ∈ 𝔠, ∀ (b : B), (algebraMap O B) c * b ∈ (algebraMap O B).range) (h_sup : 𝔠 ⊔ 𝔭 = ⊤) (h𝔭_not_contain : ¬𝔠 ≤ 𝔭) : (Ideal.map (algebraMap O B) 𝔭).IsPrime

theorem prime_bijection_coprime_conductor {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra O B] (hf : Function.Injective ⇑(algebraMap O B)) (𝔠 : Ideal O) (h𝔠_ne : 𝔠 ≠ ⊥) (h𝔠_cond : ∀ c ∈ 𝔠, ∀ (b : B), (algebraMap O B) c * b ∈ (algebraMap O B).range) (h_sup : ∀ (𝔭 : Ideal O), 𝔭.IsPrime → 𝔭 ≠ ⊥ → ¬𝔠 ≤ 𝔭 → 𝔠 ⊔ 𝔭 = ⊤) : ∃ (e : { 𝔮 : Ideal B // 𝔮.IsPrime ∧ 𝔮 ≠ ⊥ ∧ ¬Ideal.map (algebraMap O B) 𝔠 ≤ 𝔮 } ≃ { 𝔭 : Ideal O // 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ ∧ ¬𝔠 ≤ 𝔭 }), (∀ (𝔮 : { 𝔮 : Ideal B // 𝔮.IsPrime ∧ 𝔮 ≠ ⊥ ∧ ¬Ideal.map (algebraMap O B) 𝔠 ≤ 𝔮 }), ↑(e 𝔮) = Ideal.comap (algebraMap O B) ↑𝔮) ∧ ∀ (𝔭 : { 𝔭 : Ideal O // 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ ∧ ¬𝔠 ≤ 𝔭 }), ↑(e.symm 𝔭) = Ideal.map (algebraMap O B) ↑𝔭

theorem localization_equiv_coprime_conductor {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra O B] (𝔠 𝔭 : Ideal O) [h𝔭 : 𝔭.IsPrime] (h𝔭_ne : 𝔭 ≠ ⊥) : (¬𝔠 ≤ 𝔭 ↔ ∀ (x : B), x ∈ (algebraMap O B).range ↔ ∀ p ∈ 𝔭, x * (algebraMap O B) p ∈ Ideal.map (algebraMap O B) 𝔭) ∧ (¬𝔠 ≤ 𝔭 ↔ IsUnit ↑𝔭) ∧ (¬𝔠 ≤ 𝔭 ↔ IsDiscreteValuationRing (Localization.AtPrime 𝔭)) ∧ (¬𝔠 ≤ 𝔭 ↔ Submodule.IsPrincipal (IsLocalRing.maximalIdeal (Localization.AtPrime 𝔭))) ∧ (¬𝔠 ≤ 𝔭 → (Ideal.map (algebraMap O B) 𝔭).IsPrime)

theorem extendedHom_isPrimeTo_of_comap {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [IsNoetherianRing O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra O B] (hf : Function.Injective ⇑(algebraMap O B)) (𝔠 : Ideal B) (h𝔠_cond : ∀ c ∈ 𝔠, ∀ (b : B), c * b ∈ (algebraMap O B).range) (hle : nonZeroDivisors O ≤ Submonoid.comap (algebraMap O B) (nonZeroDivisors B)) (u : (FractionalIdeal (nonZeroDivisors O) (Localization (nonZeroDivisors O)))ˣ) (hu : (↑u).IsPrimeTo (Ideal.comap (algebraMap O B) 𝔠)) : (↑((Units.map ↑(FractionalIdeal.extendedHom (Localization (nonZeroDivisors B)) hle)) u)).IsPrimeTo 𝔠

theorem extended_unit_eq_one_coprime_conductor {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [IsNoetherianRing O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra O B] (hf : Function.Injective ⇑(algebraMap O B)) (𝔠 : Ideal B) (h𝔠_cond : ∀ c ∈ 𝔠, ∀ (b : B), c * b ∈ (algebraMap O B).range) (hle : nonZeroDivisors O ≤ Submonoid.comap (algebraMap O B) (nonZeroDivisors B)) (u : (FractionalIdeal (nonZeroDivisors O) (Localization (nonZeroDivisors O)))ˣ) (hu : (FractionalIdeal.extendedHom (Localization (nonZeroDivisors B)) hle) ↑u = 1) : ↑u = 1

theorem extendedHom_injective_on_units_order {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [IsNoetherianRing O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra O B] (hf : Function.Injective ⇑(algebraMap O B)) (𝔠 : Ideal B) (h𝔠_cond : ∀ c ∈ 𝔠, ∀ (b : B), c * b ∈ (algebraMap O B).range) (hle : nonZeroDivisors O ≤ Submonoid.comap (algebraMap O B) (nonZeroDivisors B)) : Function.Injective ⇑(Units.map ↑(FractionalIdeal.extendedHom (Localization (nonZeroDivisors B)) hle))

theorem surjective_preimage_helper {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [IsNoetherianRing O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra O B] (hf : Function.Injective ⇑(algebraMap O B)) (𝔠 : Ideal B) (h𝔠_cond : ∀ c ∈ 𝔠, ∀ (b : B), c * b ∈ (algebraMap O B).range) (hle : nonZeroDivisors O ≤ Submonoid.comap (algebraMap O B) (nonZeroDivisors B)) (v : ↥(invertibleFractionalIdealsPrimeTo 𝔠)) : ∃ u ∈ invertibleFractionalIdealsPrimeTo (Ideal.comap (algebraMap O B) 𝔠), (Units.map ↑(FractionalIdeal.extendedHom (Localization (nonZeroDivisors B)) hle)) u = ↑v

theorem coprime_factorization_surjective_helper {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [IsNoetherianRing O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra O B] (hf : Function.Injective ⇑(algebraMap O B)) (𝔠 : Ideal B) (h𝔠_cond : ∀ c ∈ 𝔠, ∀ (b : B), c * b ∈ (algebraMap O B).range) (hle : nonZeroDivisors O ≤ Submonoid.comap (algebraMap O B) (nonZeroDivisors B)) (v : ↥(invertibleFractionalIdealsPrimeTo 𝔠)) : ∃ (u : ↥(invertibleFractionalIdealsPrimeTo (Ideal.comap (algebraMap O B) 𝔠))), (Units.map ↑(FractionalIdeal.extendedHom (Localization (nonZeroDivisors B)) hle)) ↑u = ↑v

theorem coprime_ideal_group_iso {O : Type u_1} {B : Type u_2} [CommRing O] [IsDomain O] [IsNoetherianRing O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra O B] (hf : Function.Injective ⇑(algebraMap O B)) (𝔠 : Ideal B) (h𝔠_cond : ∀ c ∈ 𝔠, ∀ (b : B), c * b ∈ (algebraMap O B).range) : Nonempty (↥(invertibleFractionalIdealsPrimeTo (Ideal.comap (algebraMap O B) 𝔠)) ≃* ↥(invertibleFractionalIdealsPrimeTo 𝔠))

theorem coprime_residue_field_iso {A : Type u_1} {O : Type u_2} {B : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A O] [Algebra A B] [Algebra O B] [IsScalarTower A O B] (𝔮 : Ideal B) [h𝔮 : 𝔮.IsPrime] (h𝔮_ne : 𝔮 ≠ ⊥) (𝔠 : Ideal B) (h𝔮_cond : ¬𝔠 ≤ 𝔮) (h_conductor : ∀ c ∈ 𝔠, ∀ (b : B), ∃ (o : O), (algebraMap O B) o = c * b) : Nonempty (B ⧸ 𝔮 ≃+* O ⧸ Ideal.comap (algebraMap O B) 𝔮)

theorem coprime_residue_degree_eq {A : Type u_1} {O : Type u_2} {B : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A O] [Algebra A B] [Algebra O B] [IsScalarTower A O B] (𝔮 : Ideal B) [h𝔮 : 𝔮.IsPrime] (h𝔮_ne : 𝔮 ≠ ⊥) (𝔠 : Ideal B) (h𝔮_cond : ¬𝔠 ≤ 𝔮) (h_conductor : ∀ c ∈ 𝔠, ∀ (b : B), ∃ (o : O), (algebraMap O B) o = c * b) : Nat.card (B ⧸ 𝔮) = Nat.card (O ⧸ Ideal.comap (algebraMap O B) 𝔮)

theorem coprime_ideal_norm_eq {A : Type u_1} {O : Type u_2} {B : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A O] [Algebra A B] [Algebra O B] [IsScalarTower A O B] (𝔮 : Ideal B) [h𝔮 : 𝔮.IsPrime] (h𝔮_ne : 𝔮 ≠ ⊥) (𝔠 : Ideal B) (h𝔮_cond : ¬𝔠 ≤ 𝔮) (h_conductor : ∀ c ∈ 𝔠, ∀ (b : B), ∃ (o : O), (algebraMap O B) o = c * b) : Submodule.cardQuot 𝔮 = Submodule.cardQuot (Ideal.comap (algebraMap O B) 𝔮)

theorem spanNorm_le_of_conductor_coprime {A : Type u_1} {O : Type u_2} {B : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A O] [Algebra A B] [Algebra O B] [IsScalarTower A O B] [Module.Finite A B] [Module.IsTorsionFree A B] (𝔮 : Ideal B) [h𝔮 : 𝔮.IsPrime] (h𝔮_ne : 𝔮 ≠ ⊥) (𝔠 : Ideal B) (_h𝔮_cond : ¬𝔠 ≤ 𝔮) (h_conductor : ∀ c ∈ 𝔠, ∀ (b : B), ∃ (o : O), (algebraMap O B) o = c * b) (h_cond_A : ¬Ideal.comap (algebraMap A B) 𝔠 ≤ Ideal.comap (algebraMap A B) 𝔮) : Ideal.spanNorm A 𝔮 ≤ Ideal.span (⇑(Algebra.intNorm A B) '' (⇑(algebraMap O B) '' ↑(Ideal.comap (algebraMap O B) 𝔮)))

theorem coprime_norm_commutes {A : Type u_1} {O : Type u_2} {B : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A O] [Algebra A B] [Algebra O B] [IsScalarTower A O B] [Module.Finite A B] [Module.IsTorsionFree A B] (𝔮 : Ideal B) [h𝔮 : 𝔮.IsPrime] (h𝔮_ne : 𝔮 ≠ ⊥) (𝔠 : Ideal B) (h𝔮_cond : ¬𝔠 ≤ 𝔮) (h_conductor : ∀ c ∈ 𝔠, ∀ (b : B), ∃ (o : O), (algebraMap O B) o = c * b) (h_cond_A : ¬Ideal.comap (algebraMap A B) 𝔠 ≤ Ideal.comap (algebraMap A B) 𝔮) : Ideal.spanNorm A 𝔮 = Ideal.span (⇑(Algebra.intNorm A B) '' (⇑(algebraMap O B) '' ↑(Ideal.comap (algebraMap O B) 𝔮)))

theorem order_coprime_prime_properties {A : Type u_1} {O : Type u_2} {B : Type u_3} [CommRing A] [IsDomain A] [IsDedekindDomain A] [CommRing O] [IsDomain O] [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A O] [Algebra A B] [Algebra O B] [IsScalarTower A O B] [Module.Finite A B] [Module.IsTorsionFree A B] [PerfectField (FractionRing A)] (𝔮 : Ideal B) [h𝔮 : 𝔮.IsPrime] (h𝔮_ne : 𝔮 ≠ ⊥) (𝔠 : Ideal B) (h𝔮_cond : ¬𝔠 ≤ 𝔮) (h_conductor : ∀ c ∈ 𝔠, ∀ (b : B), ∃ (o : O), (algebraMap O B) o = c * b) (h_ext : 𝔠 = Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) 𝔠)) : Nat.card (B ⧸ 𝔮) = Nat.card (O ⧸ Ideal.comap (algebraMap O B) 𝔮) ∧ Submodule.cardQuot 𝔮 = Submodule.cardQuot (Ideal.comap (algebraMap O B) 𝔮) ∧ Ideal.spanNorm A 𝔮 = Ideal.span (⇑(Algebra.intNorm A B) '' (⇑(algebraMap O B) '' ↑(Ideal.comap (algebraMap O B) 𝔮))) ∧ Ideal.spanNorm A 𝔮 = Ideal.comap (algebraMap A B) 𝔮 ^ (Ideal.comap (algebraMap A B) 𝔮).inertiaDeg 𝔮