theorem
lec6_lemma13_chain
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
(α : L)
:
Key chain inequality for Lec 6, Lem 13: the number of K-conjugates of an
element α in a finite extension L/K is at most [L : K].
theorem
lec6_lemma13_fiber_card_le_degree
{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)
Lec 6, Lem 13: for a finite morphism Spec A → Spec B with B normal, the
fiber over any prime 𝔭 has at most [K(A) : K(B)] primes lying over it.
theorem
lec6_lemma13_dedekind
{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 ≠ ⊥)
:
Dedekind-domain instance of Lec 6, Lem 13: the number of primes of S lying
over a non-zero maximal p ⊆ R is bounded by [L : K].
theorem
lec6_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]
:
For a finite extension of domains, the field-of-fractions degree agrees with
the rank as a module: [K(A):K(B)] = rank_B A.