Module

ActualFiniteTameCoefficientEvaluation.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameCoefficientEvaluation

3 declarations indexed from sourceView source ↗

Module documentation

Coefficient evaluation of finite tame coordinates

Identifies the local ring map in the character composite with the finite inertia action and evaluates the ambient coordinate through a uniformizer ratio.

Imports15

Imported by2

theorem

localRingHom_eq_of_coefficient_square

L38 ↗

EtaleFundamentalGroups.Inertia.localRingHom_eq_of_coefficient_square

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w

Lean source · statement

theorem localRingHom_eq_of_coefficient_square
    (B : Type w) [CommRing B] (P : Ideal B) [P.IsPrime]
    (s : B →+* B) (hP : P = P.comap s)
    (j : Localization.AtPrime P →+* Localization.AtPrime P)
    (hj : j.comp (algebraMap B (Localization.AtPrime P)) =
      (algebraMap B (Localization.AtPrime P)).comp s) :
    j = Localization.localRingHom P P s hP

theorem

actualFiniteInertiaCompositeLocalRingHom_eq

L57 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaCompositeLocalRingHom_eq

Documentation

The coefficient map in the lower composite factorization is the SAME actual local action: the two local RingHoms agree on every coefficient.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L))

Lean source · full declaration

theorem actualFiniteInertiaCompositeLocalRingHom_eq [Q.IsPrime]
    (E : FiniteGaloisIntermediateField K L)
    (σ : actualNormalizationInertiaGroup A K L Q) :
    letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
    commAlgInertiaCompositeLocalRingHom A (finiteAbsoluteNormalizationAlgebra A K L E)
        (finiteAbsoluteNormalizationPrime A K L Q E)
        (actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ =
      actualFiniteInertiaLocalRingHom A K L Q E σ := by
  let := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
  exact localRingHom_eq_of_coefficient_square
    (finiteAbsoluteNormalizationAlgebra A K L E)
    (finiteAbsoluteNormalizationPrime A K L Q E)
    (actualFiniteNormalizationRestrictionRingHom A K L E
      (actualNormalizationInertiaElement A K L Q σ))
    (actualFiniteNormalizationRestrictionRingHom_prime A K L Q E σ)
    (commAlgInertiaCompositeLocalRingHom A (finiteAbsoluteNormalizationAlgebra A K L E)
      (finiteAbsoluteNormalizationPrime A K L Q E)
      (actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ)
    (commAlgInertiaCompositeLocalRingHom_comp_coefficient A
      (finiteAbsoluteNormalizationAlgebra A K L E)
      (finiteAbsoluteNormalizationPrime A K L Q E)
      (actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ)

theorem

actualFiniteTameCoordinate_exists_coefficient

L83 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameCoordinate_exists_coefficient

Documentation

At any uniformizer, the SAME existing ambient tame coordinate is the residue of an actual coefficient ratio raised to its original e/n exponent. The witness and the local coefficient equation are constructed together.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L))

Lean source · full declaration

theorem actualFiniteTameCoordinate_exists_coefficient
    [IsDomain A] [IsDiscreteValuationRing A] [Q.IsMaximal]
    (E : FiniteGaloisIntermediateField K L)
    (σ : actualNormalizationInertiaGroup A K L Q) :
    letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
    ∀ (π : Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E)),
      Irreducible π →
      ∃ c : Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E),
        IsUnit c ∧ π * c = (actualFiniteInertiaLocalRingHom A K L Q E σ).toFun π ∧
        (((actualFiniteTameCoordinate A K L Q E).hom'.toFun σ).val).val =
          (actualFiniteLocalResidueMap A K L Q E).toFun c ^
            ((finiteAbsoluteNormalizationPrime A K L Q E).ramificationIdx A /
              actualFiniteStageTameOrder A K L Q E) := by
  let := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
  let := finiteAbsoluteNormalizationAlgebra_isDedekindDomain A K L E
  let := finiteAbsoluteNormalizationAutomorphisms_finite A K L E
  intro π hπ
  change ∃ c : Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E),
    IsUnit c ∧ π * c = (actualFiniteInertiaLocalRingHom A K L Q E σ).toFun π ∧
    commAlgCanonicalTameCompositeValue A (finiteAbsoluteNormalizationAlgebra A K L E)
      (finiteAbsoluteNormalizationPrime A K L Q E)
      (finiteAbsoluteNormalizationPrime_ne_bot A K L Q E)
      (actualFiniteInertiaRestriction A K L Q E).hom'.toFun
      (actualFiniteNormalizationResidueMap A K L Q E) σ =
        (actualFiniteLocalResidueMap A K L Q E).toFun c ^
          ((finiteAbsoluteNormalizationPrime A K L Q E).ramificationIdx A /
            actualFiniteStageTameOrder A K L Q E)
  obtain ⟨c, hc, hπc, hvalue⟩ :=
    commAlgCanonicalTameCompositeValue_exists_coefficient A
      (finiteAbsoluteNormalizationAlgebra A K L E)
      (finiteAbsoluteNormalizationPrime A K L Q E)
      (finiteAbsoluteNormalizationPrime_ne_bot A K L Q E)
      (actualFiniteInertiaRestriction A K L Q E).hom'.toFun
      (actualFiniteNormalizationResidueMap A K L Q E) π hπ σ
  refine ⟨c, hc, ?_, ?_⟩
  · exact hπc.trans (congrArg
      (fun f : Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E) →+*
          Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E) => f.toFun π)
      (actualFiniteInertiaCompositeLocalRingHom_eq A K L Q E σ))
  · have hi :
        (actualFiniteNormalizationResidueMap A K L Q E).toFun
            ((IsLocalRing.residue
              (Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E))).toFun c) =
          (actualFiniteLocalResidueMap A K L Q E).toFun c :=
      (congrArg
        (fun f : Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E) →+*
            Q.ResidueField => f.toFun c)
        (actualFiniteLocalResidueMap_eq_residueMap_comp A K L Q E)).symm
    exact hvalue.trans (congrArg
      (fun x : Q.ResidueField => x ^
        ((finiteAbsoluteNormalizationPrime A K L Q E).ramificationIdx A /
          actualFiniteStageTameOrder A K L Q E)) hi)

Module documentation

Coefficient evaluation of finite tame coordinates

Declarations

localRingHom_eq_of_coefficient_square

actualFiniteInertiaCompositeLocalRingHom_eq

actualFiniteTameCoordinate_exists_coefficient