Documentation

Atlas.NumberTheoryI.code.PrimeSplitting

theorem liesOver_of_dvd_map {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra A B] {p : Ideal A} {P : Ideal B} [hp : p.IsMaximal] [hP : P.IsPrime] (hdvd : P ∣ Ideal.map (algebraMap A B) p) :

theorem dvd_map_of_liesOver {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra A B] {p : Ideal A} {P : Ideal B} [hlo : P.LiesOver p] :

P ∣ Ideal.map (algebraMap A B) p

theorem dvd_map_iff_liesOver {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra A B] {p : Ideal A} {P : Ideal B} [hp : p.IsMaximal] [hP : P.IsPrime] :

P ∣ Ideal.map (algebraMap A B) p ↔ P.LiesOver p

theorem ramificationIdx_def {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) :

p.ramificationIdx P = sSup {n : ℕ | Ideal.map (algebraMap A B) p ≤ P ^ n}

theorem inertiaDeg_def {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] :

p.inertiaDeg P = Module.finrank (A ⧸ p) (B ⧸ P)

theorem ramificationIdx_mul_tower {A : Type u_1} [CommRing A] [IsDomain A] {B : Type u_2} [CommRing B] [IsDedekindDomain B] {C : Type u_3} [CommRing C] [IsDedekindDomain C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [Module.IsTorsionFree A B] [Module.IsTorsionFree B C] (p : Ideal A) (P : Ideal B) (Q : Ideal C) [Q.IsPrime] [Q.LiesOver P] [P.LiesOver p] :

p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q

theorem inertiaDeg_mul_tower {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {C : Type u_3} [CommRing C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (p : Ideal A) (P : Ideal B) (Q : Ideal C) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p] [Q.LiesOver P] :

p.inertiaDeg Q = p.inertiaDeg P * P.inertiaDeg Q

theorem ramificationIdx_inertiaDeg_mul_tower {A : Type u_1} [CommRing A] [IsDomain A] {B : Type u_2} [CommRing B] [IsDedekindDomain B] {C : Type u_3} [CommRing C] [IsDedekindDomain C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [Module.IsTorsionFree A B] [Module.IsTorsionFree B C] (p : Ideal A) (P : Ideal B) (Q : Ideal C) [p.IsMaximal] [P.IsMaximal] [Q.IsPrime] [Q.LiesOver P] [P.LiesOver p] :

p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q ∧ p.inertiaDeg Q = p.inertiaDeg P * P.inertiaDeg Q

@[deprecated ramificationIdx_inertiaDeg_mul_tower (since := "2025-05-04")]

theorem lemma_5_30 {A : Type u_1} [CommRing A] [IsDomain A] {B : Type u_2} [CommRing B] [IsDedekindDomain B] {C : Type u_3} [CommRing C] [IsDedekindDomain C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [Module.IsTorsionFree A B] [Module.IsTorsionFree B C] (p : Ideal A) (P : Ideal B) (Q : Ideal C) [p.IsMaximal] [P.IsMaximal] [Q.IsPrime] [Q.LiesOver P] [P.LiesOver p] :

p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q ∧ p.inertiaDeg Q = p.inertiaDeg P * P.inertiaDeg Q

theorem isIntegralClosure_tower_top (A : Type u_1) [CommRing A] (B : Type u_2) [CommRing B] (C : Type u_3) [CommRing C] (M : Type u_4) [CommRing M] [Algebra A B] [Algebra A M] [Algebra B M] [Algebra C M] [IsScalarTower A B M] [IsIntegralClosure C A M] [Algebra.IsIntegral A B] :

IsIntegralClosure C B M

@[deprecated isIntegralClosure_tower_top (since := "2025-05-04")]

theorem lemma_5_30_integral_closure (A : Type u_1) [CommRing A] (B : Type u_2) [CommRing B] (C : Type u_3) [CommRing C] (M : Type u_4) [CommRing M] [Algebra A B] [Algebra A M] [Algebra B M] [Algebra C M] [IsScalarTower A B M] [IsIntegralClosure C A M] [Algebra.IsIntegral A B] :

IsIntegralClosure C B M

theorem dim_quotient_eq_finrank {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Type u_2} [CommRing S] [IsDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] [Module.Finite R S] (p : Ideal R) [p.IsMaximal] :

Module.finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = Module.finrank K L

theorem sum_ef_eq_degree {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :

∑ P ∈ primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P = Module.finrank K L

theorem ramificationIdx_pos {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [P.IsPrime] [P.LiesOver p] (hp0 : p ≠ ⊥) :

1 ≤ p.ramificationIdx P

theorem ramificationIdx_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [P.IsPrime] [P.LiesOver p] :

p.ramificationIdx P ≤ Module.finrank K L

theorem inertiaDeg_pos {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] [Module.Finite R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [P.IsPrime] [P.LiesOver p] :

1 ≤ p.inertiaDeg P

theorem inertiaDeg_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [P.IsPrime] [P.LiesOver p] (hp0 : p ≠ ⊥) :

p.inertiaDeg P ≤ Module.finrank K L

theorem card_primes_over_pos {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :

1 ≤ (primesOverFinset p S).card

theorem card_primes_over_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :

(primesOverFinset p S).card ≤ Module.finrank K L

def IsTotallyRamified {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] (p : Ideal A) (P : Ideal B) :

Instances For

def IsUnramifiedAt {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] :

Instances For

def IsInert {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] (p : Ideal A) :

Instances For

def SplitsCompletely {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra A B] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] (p : Ideal A) :

Instances For