Module

ActualFiniteInertiaSurjectivity.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteInertiaSurjectivity

2 declarations indexed from sourceView source ↗

Module documentation

Surjectivity onto actual finite-normalization inertia

An intrinsic finite-normalization inertia element first lifts to the actual finite Galois group. The proved profinite inertia image then lifts it to the original, possibly infinite normalization inertia. Both lifts use the existing restriction maps.

Imports4

Imported by5

theorem

finiteNormalizationInertia_exists_finiteNative_lift

L34 ↗

EtaleFundamentalGroups.Inertia.finiteNormalizationInertia_exists_finiteNative_lift

Documentation

Intrinsic finite inertia has a lift for the actual finite field action. The finite field structure remains closed in its native owner.

Source context 4 commands

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

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]

Lean source · statement

theorem finiteNormalizationInertia_exists_finiteNative_lift
    (Q : Ideal (integralClosure A L)) (E : FiniteGaloisIntermediateField K L)
    (τ : (commAlgIdealInertiaGroup A (finiteAbsoluteNormalizationAlgebra A K L E)
      (finiteAbsoluteNormalizationPrime A K L Q E)).carrier) :
    ∃ g : { g : (finiteGaloisGroupObject K L E).carrier //
      ((finiteNormalizationActionDiagram A K L E).lowerInertia
        (finiteAbsoluteNormalizationPrime A K L Q E)).carrier g },
      (finiteNormalizationGaloisGroupMap A K L E).hom'.toFun g.val = τ.val

theorem

actualFiniteInertiaRestriction_surjective

L52 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaRestriction_surjective