AnabelianGeometry.GeometricFundamentalGroup.ramificationIndex_eq_one_of_unramified_restrictInclusion
An unramified, essentially finite type inclusion of valuation rings has ramification index one, measured in the original field extension.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicCurve IsLocalRing IsDedekindDomain
namespace AnabelianGeometry.GeometricFundamentalGroupLean source · full declaration
theorem ramificationIndex_eq_one_of_unramified_restrictInclusion
{K F E : Type*} [Field K] [Field F] [Field E]
[Algebra K F] [Algebra K E] [Algebra F E] [IsScalarTower K F E]
[Algebra.IsIntegral F E] (w : Place K E) :
let _ := (w.restrictInclusion F).toAlgebra
Algebra.EssFiniteType (w.restrict F).toValuationSubring w.toValuationSubring →
Algebra.FormallyUnramified (w.restrict F).toValuationSubring w.toValuationSubring →
w.ramificationIndex F = 1 := by
intro valuationAlgebra finiteType unramified
have localMap : IsLocalHom
(algebraMap (w.restrict F).toValuationSubring w.toValuationSubring) :=
show IsLocalHom (w.restrictInclusion F) from inferInstance
obtain ⟨t, ht⟩ := IsDiscreteValuationRing.exists_irreducible
(w.restrict F).toValuationSubring
have imageNeZero : w.restrictInclusion F t ≠ 0 := by
intro h
have hc := congrArg Subtype.val h
rw [Place.coe_restrictInclusion] at hc
exact ht.ne_zero (Subtype.ext ((map_eq_zero (algebraMap F E)).mp hc))
have imageIdeal : Ideal.span {w.restrictInclusion F t} =
maximalIdeal w.toValuationSubring := by
have h := Algebra.FormallyUnramified.map_maximalIdeal
(R := (w.restrict F).toValuationSubring) (S := w.toValuationSubring)
rw [ht.maximalIdeal_eq, Ideal.map_span, Set.image_singleton] at h
exact h
have imageIrreducible : Irreducible (w.restrictInclusion F t) :=
Ideal.irreducible_of_isMaximal_span_singleton imageNeZero
(imageIdeal ▸ maximalIdeal.isMaximal w.toValuationSubring)
have imageOrder := w.ord_coe_irreducible imageIrreducible
rw [Place.coe_restrictInclusion, w.ord_restrict,
(w.restrict F).ord_coe_irreducible ht, mul_one] at imageOrder
exact_mod_cast imageOrder