Module

FiniteGaloisRestrictionContinuity.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteGaloisRestrictionContinuity

1 declaration indexed from sourceView source ↗

Module documentation

Local constancy of the actual finite Galois restriction

The domain keeps its original Krull topology. Finite dimensionality makes the target's Krull topology discrete, so the existing continuous restriction is locally constant before any normalization or coefficient action is opened.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.FiniteGaloisRestrictionGroupMap
Nyll.EtaleFundamentalGroups.Inertia.NativeGaloisGroupTopology
Mathlib.FieldTheory.Galois.Profinite
Mathlib.Topology.LocallyConstant.Basic

Imported by2

theorem

finiteGaloisRestrictionGroupMap_isLocallyConstant

L26 ↗

EtaleFundamentalGroups.Inertia.finiteGaloisRestrictionGroupMap_isLocallyConstant

Documentation

The actual finite Galois restriction is locally constant for the original Krull topology, using the target's finite-dimensional discrete topology.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem finiteGaloisRestrictionGroupMap_isLocallyConstant
    (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
    (E : FiniteGaloisIntermediateField K L) :
    IsLocallyConstant (finiteGaloisRestrictionGroupMap K L E).hom'.toFun

Module documentation

Local constancy of the actual finite Galois restriction

Declarations

finiteGaloisRestrictionGroupMap_isLocallyConstant