theorem
function_field_separable_of_smooth_curves
(k : Type u_1)
[Field k]
(R : Type u_2)
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
[Algebra k R]
(S : Type u_3)
[CommRing S]
[IsDomain S]
[IsDedekindDomain S]
[Algebra k S]
[Algebra R S]
[IsScalarTower k R S]
[NoZeroSMulDivisors R S]
[Module.Finite R S]
(K : Type u_4)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(L : Type u_5)
[Field L]
[Algebra S L]
[IsFractionRing S L]
[Algebra K L]
[Algebra R L]
[IsScalarTower R S L]
[IsScalarTower R K L]
[Algebra k K]
[Algebra k L]
[IsScalarTower k R K]
[IsScalarTower k S L]
:
For a finite morphism of smooth curves over k, the induced extension
of function fields is separable.
theorem
mapBaseChange_iso_different_smul_kaehler
(k : Type u_1)
[Field k]
(R : Type u_2)
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
[Algebra k R]
(S : Type u_3)
[CommRing S]
[IsDomain S]
[IsDedekindDomain S]
[Algebra k S]
[Algebra R S]
[IsScalarTower k R S]
[NoZeroSMulDivisors R S]
[Module.Finite R S]
[Algebra (FractionRing R) (FractionRing S)]
[Algebra.IsSeparable (FractionRing R) (FractionRing S)]
(hTame :
∀ (P : Ideal S) [P.IsMaximal],
((Ideal.comap (algebraMap R S) P).ramificationIdx P).Coprime (ringChar k) ∨ ringChar k = 0)
:
Nonempty (TensorProduct R S Ω[R⁄k] ≃ₗ[S] ↥(differentIdeal R S • ⊤))
Base-change identification: under tameness, the base-changed Kähler module
S ⊗_R Ω_{R/k} is isomorphic to the submodule 𝔡 · Ω_{S/k} of Ω_{S/k}.
theorem
kaehler_tensor_ideal_iso_smul
(k : Type u_1)
[Field k]
(R : Type u_2)
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
[Algebra k R]
(S : Type u_3)
[CommRing S]
[IsDomain S]
[IsDedekindDomain S]
[Algebra k S]
[Algebra R S]
[IsScalarTower k R S]
[NoZeroSMulDivisors R S]
[Module.Finite R S]
[Algebra (FractionRing R) (FractionRing S)]
[Algebra.IsSeparable (FractionRing R) (FractionRing S)]
:
Nonempty (TensorProduct S Ω[S⁄k] ↥(differentIdeal R S) ≃ₗ[S] ↥(differentIdeal R S • ⊤))
The tensor product Ω_{S/k} ⊗_S 𝔡 is S-linearly isomorphic to
𝔡 · Ω_{S/k}, the scaled submodule of Kähler differentials.
theorem
riemann_hurwitz_sheaf_iso
(k : Type u_1)
[Field k]
(R : Type u_2)
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
[Algebra k R]
(S : Type u_3)
[CommRing S]
[IsDomain S]
[IsDedekindDomain S]
[Algebra k S]
[Algebra R S]
[IsScalarTower k R S]
[NoZeroSMulDivisors R S]
[Module.Finite R S]
[Algebra (FractionRing R) (FractionRing S)]
[Algebra.IsSeparable (FractionRing R) (FractionRing S)]
(hTame :
∀ (P : Ideal S) [P.IsMaximal],
((Ideal.comap (algebraMap R S) P).ramificationIdx P).Coprime (ringChar k) ∨ ringChar k = 0)
:
Nonempty (TensorProduct S Ω[S⁄k] ↥(differentIdeal R S) ≃ₗ[S] TensorProduct R S Ω[R⁄k])
Riemann–Hurwitz sheaf isomorphism (Thm 21.1 sheaf form): under tameness,
Ω_{S/k} ⊗_S 𝔡_{S/R} is S-linearly isomorphic to S ⊗_R Ω_{R/k}.
theorem
local_ramification_nonneg
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{S : Type u_2}
[CommRing S]
[IsDomain S]
[IsDedekindDomain S]
[Algebra R S]
[NoZeroSMulDivisors R S]
{p : Ideal R}
[p.IsMaximal]
(hp0 : p ≠ ⊥)
:
The local ramification contribution ∑_{P|p}(e_P - 1) is non-negative.
theorem
local_ramification_le_finrank
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{S : Type u_2}
[CommRing S]
[IsDomain S]
[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 ≠ ⊥)
:
The local ramification contribution at p is bounded by the field
extension degree [L : K].
theorem
local_ramification_eq_zero_iff
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{S : Type u_2}
[CommRing S]
[IsDomain S]
[IsDedekindDomain S]
[Algebra R S]
[NoZeroSMulDivisors R S]
{p : Ideal R}
[p.IsMaximal]
(hp0 : p ≠ ⊥)
:
∑ P ∈ primesOverFinset p S, (↑(p.ramificationIdx P) - 1) = 0 ↔ ∀ P ∈ primesOverFinset p S, p.ramificationIdx P = 1
The local ramification contribution vanishes iff every prime above p
has ramification index 1 (i.e. p is unramified).
theorem
DVR_ef_product_eq_degree
{R : Type u_3}
[CommRing R]
[IsDomain R]
[IsDiscreteValuationRing R]
{S : Type u_4}
[CommRing S]
[IsDomain S]
[IsDiscreteValuationRing S]
[Algebra R S]
(K : Type u_5)
(L : Type u_6)
[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]
[IsDedekindDomain R]
[IsDedekindDomain S]
(hp0 : IsLocalRing.maximalIdeal R ≠ ⊥)
:
For an extension R ⊆ S of DVRs with fraction fields K ⊆ L, the
identity e · f = [L : K] holds.