Module

AffineNormalizationRamification.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.AffineNormalizationRamification

1 declaration indexed from sourceView source ↗

Module documentation

Ramification above an etale affine normalization

A place whose valuation ring contains a Dedekind affine coordinate ring has an actual centre in that affine chart. Localizing the normalization at this centre identifies its base with the valuation ring, so etaleness on the chart implies ramification index one.

Imports4

Imported by3

theorem

ramificationIndex_eq_one_of_etale_affine_normalization

L30 ↗

AnabelianGeometry.GeometricFundamentalGroup.ramificationIndex_eq_one_of_etale_affine_normalization

Documentation

An etale affine normalization is unramified at every place centred on the chart. The valuation-ring comparison is constructed from the centre, not assumed.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicCurve IsDedekindDomain EtaleFundamentalGroups
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u

Lean source · statement

theorem ramificationIndex_eq_one_of_etale_affine_normalization
    {K R F E : Type u} [Field K] [CommRing R] [IsDedekindDomain R]
    [Field F] [Field E] [Algebra K F] [Algebra K E]
    [Algebra R F] [IsFractionRing R F] [Algebra F E]
    [Algebra R E] [IsScalarTower R F E] [IsScalarTower K F E]
    [FiniteDimensional F E] [Algebra.IsSeparable F E]
    (hEtale : Algebra.Etale R (integralClosure R E))
    (w : Place K E)
    (hcentre : ∀ r : R, algebraMap R F r ∈ (w.restrict F).toValuationSubring) :
    w.ramificationIndex F = 1

Module documentation

Ramification above an etale affine normalization

Declarations

ramificationIndex_eq_one_of_etale_affine_normalization