NYLL
Module

StandardCover.lean

Nyll.EtaleFundamentalGroups.Kummer.AdjoinRoot.StandardCover
2 declarations indexed from sourceView source ↗

Module documentation

The standard Kummer morphism and its étale restriction

For a positive exponent n invertible in A, the actual map Spec (A[X] / (X ^ n - f)) → Spec A is finite, flat, and locally of finite presentation, with rank n at every point. Its coordinate algebra is free. The actual localization map A_f → (A[X] / (X ^ n - f))_f is finite étale.

The étale proof identifies the localization map itself with the scalar extension of the root equation. The equivalence is checked on coefficients before transporting étaleness, so it respects the specified maps of rings.

This supplies the finite-locally-free and étale-away conclusions of Stacks Project, Example 58.31.4. The codimension-one normalization and ramification calculations are in ReducedBoundary; the scheme-level tame conclusion is not asserted here. https://stacks.math.columbia.edu/tag/0EYF

Imports24
  • Mathlib.Algebra.Polynomial.AlgebraMap
  • Mathlib.Algebra.Polynomial.Degree.Operations
  • Mathlib.AlgebraicGeometry.Morphisms.Etale
  • Mathlib.AlgebraicGeometry.Morphisms.Finite
  • Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
  • Mathlib.AlgebraicGeometry.Morphisms.Flat
  • Mathlib.AlgebraicGeometry.Morphisms.FlatRank
  • Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
  • Mathlib.LinearAlgebra.Dimension.StrongRankCondition
  • Mathlib.RingTheory.AdjoinRoot
  • Mathlib.RingTheory.Etale.Basic
  • Mathlib.RingTheory.Flat.Basic
  • Mathlib.RingTheory.Localization.Away.Basic
  • Mathlib.RingTheory.Localization.BaseChange
  • Mathlib.RingTheory.Localization.Defs
  • Mathlib.RingTheory.RingHom.Etale
  • Mathlib.RingTheory.RingHom.Finite
  • Mathlib.RingTheory.RingHom.FinitePresentation
  • Mathlib.RingTheory.RingHom.Flat
  • Mathlib.RingTheory.Spectrum.Prime.FreeLocus
  • Mathlib.RingTheory.Spectrum.Prime.Basic
  • Mathlib.RingTheory.TensorProduct.Maps
  • Nyll.EtaleFundamentalGroups.Kummer.AdjoinRoot.FormallyEtale
  • Nyll.EtaleFundamentalGroups.Kummer.UnitAbsorption.HigherRadicalActualFactor
Imported by1

Declarations

theorem

finite_etale_awayMap_adjoinRoot

L62 ↗
EtaleFundamentalGroups.Kummer.finite_etale_awayMap_adjoinRoot
Documentation

Inverting the radicand in the original root algebra gives a finite étale map from the corresponding localization of the original base.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial AlgebraicGeometry
open scoped TensorProduct
universe u
Lean source · full declaration
theorem finite_etale_awayMap_adjoinRoot
    {A : Type u} [CommRing A] {n : ℕ} (hn : 0 < n)
    (hnUnit : IsUnit (n : A)) (f : A) :
    let B := AdjoinRoot (X ^ n - C f)
    (Localization.awayMap (algebraMap A B) f).Finite ∧
      (Localization.awayMap (algebraMap A B) f).Etale := by
  intro B
  have : Module.Finite A B := (Polynomial.monic_X_pow_sub_C f hn.ne').finite_adjoinRoot
  refine ⟨RingHom.localization_away_map_finite A B
    (Localization.Away f) (Localization.Away (algebraMap A B f))
    (algebraMap A B) f (RingHom.finite_algebraMap.mpr inferInstance), ?_⟩
  let Af := Localization.Away f
  let Bf := Localization.Away (algebraMap A B f)
  let T := Af ⊗[A] B
  let D := AdjoinRoot (X ^ n - C (algebraMap A Af f))
  let eRoot : T ≃ₐ[Af] D :=
    (adjoinRootBaseChangeAlgEquiv (S := Af) (X ^ n - C f)).trans
      (AdjoinRoot.algEquivOfEq Af _ _ (by
        rw [Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_C]))
  have hformal : Algebra.FormallyEtale Af D :=
    formallyEtale_adjoinRoot_X_pow_sub_C hn
      (by simpa only [map_natCast] using hnUnit.map (algebraMap A Af))
      (IsLocalization.Away.algebraMap_isUnit f)
  have : Algebra.Etale Af D := { formallyEtale := hformal }
  have : Algebra.Etale Af T := Algebra.Etale.of_equiv eRoot.symm
  let : Algebra B T := Algebra.TensorProduct.rightAlgebra
  let eAway : T ≃ₐ[B] Bf :=
    IsLocalization.Away.tensorRightEquiv (R := A) (S := B) (r := f) (A := Af)
  have hmap : eAway.toRingHom.comp (algebraMap Af T) =
      Localization.awayMap (algebraMap A B) f := by
    apply IsLocalization.ringHom_ext (Submonoid.powers f)
    ext a
    change eAway (algebraMap A Af a ⊗ₜ[A] (1 : B)) =
      Localization.awayMap (algebraMap A B) f (algebraMap A Af a)
    rw [Algebra.TensorProduct.tmul_one_eq_one_tmul]
    change eAway (algebraMap B T (algebraMap A B a)) = _
    rw [eAway.commutes]
    change algebraMap B Bf (algebraMap A B a) =
      IsLocalization.map Bf (algebraMap A B) _ (algebraMap A Af a)
    symm
    exact IsLocalization.map_eq _ a
  rw [← hmap]
  exact RingHom.Etale.respectsIso.1 (algebraMap Af T) eAway.toRingEquiv
    (RingHom.etale_algebraMap.mpr inferInstance)
theorem

standardKummerCover_finiteFlat_and_etaleAway

L114 ↗
EtaleFundamentalGroups.Kummer.standardKummerCover_finiteFlat_and_etaleAway
Documentation

The literal standard Kummer morphism is finite locally free of rank n, expressed by freeness of its affine coordinate algebra and the native finite, flat, finite-presentation, and scheme-rank predicates. Its literal localization away from f is finite étale.

The ambient ring may be reducible or even the zero ring; the rank assertion is quantified over its points.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial AlgebraicGeometry
open scoped TensorProduct
universe u
Lean source · full declaration
theorem standardKummerCover_finiteFlat_and_etaleAway
    {A : Type u} [CommRing A] {n : ℕ} (hn : 0 < n)
    (hnUnit : IsUnit (n : A)) (f : A) :
    let B := AdjoinRoot (X ^ n - C f)
    let π := Spec.map (CommRingCat.ofHom (algebraMap A B))
    let πAway := Spec.map (CommRingCat.ofHom (Localization.awayMap (algebraMap A B) f))
    Module.Free A B ∧ IsFinite π ∧ Flat π ∧ LocallyOfFinitePresentation π ∧
      (∀ x : PrimeSpectrum A, π.finrank x = n) ∧ IsFinite πAway ∧ Etale πAway := by
  intro B π πAway
  have hmonic : (X ^ n - C f).Monic := Polynomial.monic_X_pow_sub_C f hn.ne'
  have : Module.Free A B := hmonic.free_adjoinRoot
  have : Module.Finite A B := hmonic.finite_adjoinRoot
  have hfinite : IsFinite π :=
    (IsFinite.SpecMap_iff (CommRingCat.ofHom (algebraMap A B))).mpr
      (RingHom.finite_algebraMap.mpr inferInstance)
  have hflat : Flat π := Flat.SpecMap_iff.mpr
    (RingHom.flat_algebraMap_iff.mpr inferInstance)
  have hfp : LocallyOfFinitePresentation π :=
    (LocallyOfFinitePresentation.SpecMap_iff
      (CommRingCat.ofHom (algebraMap A B))).mpr
        (RingHom.finitePresentation_algebraMap.mpr inferInstance)
  obtain ⟨hAwayFinite, hAwayEtale⟩ := finite_etale_awayMap_adjoinRoot hn hnUnit f
  refine ⟨inferInstance, hfinite, hflat, hfp, ?_, ?_, ?_⟩
  · intro x
    have : Nontrivial A := x.nontrivial
    change (Spec.map (CommRingCat.ofHom (algebraMap A B))).finrank x = n
    rw [Scheme.Hom.finrank_SpecMap_algebraMap, Module.rankAtStalk_eq_finrank_of_free]
    change Module.finrank A B = n
    rw [Module.finrank_eq_card_basis (AdjoinRoot.powerBasisAux' hmonic),
      Fintype.card_fin, Polynomial.natDegree_X_pow_sub_C]
  · exact (IsFinite.SpecMap_iff
      (CommRingCat.ofHom (Localization.awayMap (algebraMap A B) f))).mpr hAwayFinite
  · exact (HasRingHomProperty.Spec_iff (P := @Etale)).mpr hAwayEtale

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.