Module

ActualFiniteQuotientTameValueTower.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteQuotientTameValueTower

3 declarations indexed from sourceView source ↗

Module documentation

Actual quotient-scalar compatibility over every divisible pair of degrees

The common-upper-stage calculation uses the existing normalized raw maps. No finite root group is opened while the third finite stage is in scope.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteQuotientTameValue
Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameCoordinateTower
Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameOrderTower
Mathlib.FieldTheory.Galois.GaloisClosure

Imported by3

theorem

actualFiniteTameNormalizationMap_pow_of_dvd

L35 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameNormalizationMap_pow_of_dvd

Documentation

Common finite upper stages prove the scalar power law independently of an inclusion between the two selected finite fields.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing 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).carrier) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteTameNormalizationMap_pow_of_dvd
    (E F : FiniteGaloisIntermediateField K L)
    (h : actualFiniteStageTameOrder A K L Q E ∣ actualFiniteStageTameOrder A K L Q F)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    (actualFiniteTameNormalizationMap A K L Q F).toFun
        (actualFiniteRawTameValue A K L Q F σ) ^
        (actualFiniteStageTameOrder A K L Q F / actualFiniteStageTameOrder A K L Q E) =
      (actualFiniteTameNormalizationMap A K L Q E).toFun
        (actualFiniteRawTameValue A K L Q E σ)

theorem

actualFiniteQuotientTameValue_pow_of_dvd

L53 ↗

EtaleFundamentalGroups.Inertia.actualFiniteQuotientTameValue_pow_of_dvd

Documentation

The scalar of the SAME quotient coordinate obeys every actual degree divisibility relation.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing 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).carrier) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteQuotientTameValue_pow_of_dvd
    (E F : FiniteGaloisIntermediateField K L)
    (h : actualFiniteStageTameOrder A K L Q E ∣ actualFiniteStageTameOrder A K L Q F)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    actualFiniteQuotientTameValue A K L Q F σ ^
        (actualFiniteStageTameOrder A K L Q F / actualFiniteStageTameOrder A K L Q E) =
      actualFiniteQuotientTameValue A K L Q E σ

theorem

actualFiniteQuotientTameValue_eq_of_tameOrder_eq

L71 ↗

EtaleFundamentalGroups.Inertia.actualFiniteQuotientTameValue_eq_of_tameOrder_eq

Documentation

Equal actual degrees give equal quotient scalars, independently of which finite Galois stage realizes the degree.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing 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).carrier) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteQuotientTameValue_eq_of_tameOrder_eq
    (E F : FiniteGaloisIntermediateField K L)
    (h : actualFiniteStageTameOrder A K L Q E = actualFiniteStageTameOrder A K L Q F)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    actualFiniteQuotientTameValue A K L Q E σ =
      actualFiniteQuotientTameValue A K L Q F σ

Module documentation

Actual quotient-scalar compatibility over every divisible pair of degrees

Declarations

actualFiniteTameNormalizationMap_pow_of_dvd

actualFiniteQuotientTameValue_pow_of_dvd

actualFiniteQuotientTameValue_eq_of_tameOrder_eq