noncomputable def FiberDegreeBound.degree (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain A] [Algebra B A] [FaithfulSMul B A] : ℕ

The degree of a finite morphism of integral domains, defined as the rank of fraction fields [K(A) : K(B)].

theorem FiberDegreeBound.degree_eq_finrank (B : Type u_1) (A : Type u_2) [CommRing B] [IsDomain B] [CommRing A] [IsDomain A] [Algebra B A] [FaithfulSMul B A] [Module.Finite B A] : degree B A = Module.finrank B A

For a finite extension of domains, degree coincides with the module rank.

theorem FiberDegreeBound.lec6_fiber_card_le_degree_general {B : Type u_1} [CommRing B] [IsDomain B] [IsNoetherianRing B] [IsIntegrallyClosed B] {A : Type u_2} [CommRing A] [IsDomain A] [Algebra B A] [Module.Finite B A] [NoZeroSMulDivisors B A] (𝔭 : Ideal B) [𝔭.IsPrime] : Nat.card ↑{q : Ideal A | q.IsPrime ∧ Ideal.comap (algebraMap B A) q = 𝔭} ≤ Module.finrank (FractionRing B) (FractionRing A)

General version of Lec 6, Lem 13: over a normal Noetherian base B, the fiber of a finite morphism Spec A → Spec B has cardinality bounded by the generic degree [K(A) : K(B)].

theorem FiberDegreeBound.fdb_fiber_card_le_degree {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors 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 ≠ ⊥) : (primesOverFinset p S).card ≤ Module.finrank K L

Specialization of the fiber bound to Dedekind domains: the number of primes of S lying over a non-zero maximal p ⊂ R is at most [L : K].

theorem FiberDegreeBound.fdb_fundamental_identity {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [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

The fundamental identity Σ e_i f_i = [L : K] for primes lying over a non-zero maximal ideal in a Dedekind extension.

def FiberDegreeBound.FdbIsUnramifiedOver (B : Type u_1) (A : Type u_2) [CommRing B] [IsDomain B] [CommRing A] [IsDomain A] [Algebra B A] [NoZeroSMulDivisors B A] (𝔭 : Ideal B) : Prop

Spec A → Spec B is unramified over 𝔭 when the fiber attains the degree upper bound (i.e. the fiber bound of Lem 13 is an equality).

def FiberDegreeBound.FdbIsRamifiedOver (B : Type u_1) (A : Type u_2) [CommRing B] [IsDomain B] [CommRing A] [IsDomain A] [Algebra B A] [NoZeroSMulDivisors B A] (𝔭 : Ideal B) : Prop

Spec A → Spec B is ramified over 𝔭 when the fiber bound is a strict inequality.

def FiberDegreeBound.FdbIsUnramifiedAt {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) [Field K] (L : Type u_4) [Field L] [Algebra K L] (p : Ideal R) [p.IsMaximal] : Prop

Dedekind-domain version of unramifiedness: the number of primes over p equals [L : K].

def FiberDegreeBound.FdbIsRamifiedAt {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) [Field K] (L : Type u_4) [Field L] [Algebra K L] (p : Ideal R) [p.IsMaximal] : Prop

The Dedekind-domain ramified condition: the fiber bound at p is strict.

theorem FiberDegreeBound.fdb_isRamifiedAt_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [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 ≠ ⊥) : FdbIsRamifiedAt K L p ↔ (primesOverFinset p S).card < Module.finrank K L

Ramification at p is equivalent to a strict inequality in the fiber bound.

theorem FiberDegreeBound.fdb_unramified_implies_all_ef_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [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 ≠ ⊥) (hunr : FdbIsUnramifiedAt K L p) (P : Ideal S) : P ∈ primesOverFinset p S → p.ramificationIdx P = 1 ∧ p.inertiaDeg P = 1

If p is unramified (fiber bound is an equality), then every e_P · f_P = 1, i.e. e_P = f_P = 1 for each prime P over p.

theorem FiberDegreeBound.fdb_all_ef_one_implies_unramified {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [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 ≠ ⊥) (hef : ∀ P ∈ primesOverFinset p S, p.ramificationIdx P = 1 ∧ p.inertiaDeg P = 1) : FdbIsUnramifiedAt K L p

Converse: if every prime over p has e = f = 1, then p is unramified.

theorem FiberDegreeBound.fdb_isUnramifiedAt_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [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 ≠ ⊥) : FdbIsUnramifiedAt K L p ↔ ∀ P ∈ primesOverFinset p S, p.ramificationIdx P = 1 ∧ p.inertiaDeg P = 1

Characterization: p is unramified iff every prime over p has trivial ramification index and inertia degree.

theorem FiberDegreeBound.fdb_inertiaDeg_le_degree {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [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] (P : Ideal S) [P.IsPrime] [P.LiesOver p] (hp0 : p ≠ ⊥) : p.inertiaDeg P ≤ Module.finrank K L

Each inertia degree f_P is bounded by the global degree [L : K].

theorem FiberDegreeBound.fdb_ramificationIdx_le_degree {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [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] (P : Ideal S) [P.IsPrime] [P.LiesOver p] : p.ramificationIdx P ≤ Module.finrank K L

Each ramification index e_P is bounded by the global degree [L : K].