Module

ActualFiniteTameCoordinateKernel.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameCoordinateKernel

2 declarations indexed from sourceView source ↗

Module documentation

Kernels of the actual finite coordinates on original inertia

The ambient residue-field embedding is injective. Composing it with the SAME normalized finite character therefore leaves the actual wild kernel unchanged, before pulling it back through original inertia restriction.

Imports14

Imported by2

theorem

actualFiniteRootsGroupMap_injective

L43 ↗

EtaleFundamentalGroups.Inertia.actualFiniteRootsGroupMap_injective

Documentation

The actual coefficient embedding is injective on its actual roots group.

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] [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 actualFiniteRootsGroupMap_injective (E : FiniteGaloisIntermediateField K L) :
    Function.Injective (actualFiniteRootsGroupMap A K L Q E).hom'.toFun

theorem