Module

ActualFiniteInertiaSeparation.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteInertiaSeparation

1 declaration indexed from sourceView source ↗

Module documentation

Actual finite inertia restrictions separate original inertia

Finite normalization faithfulness and finite Galois closure separation are both proved from the original inputs. No separation premise is added.

Imports6

Imported by3

theorem

actualFiniteInertiaRestriction_jointly_injective

L29 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaRestriction_jointly_injective

Documentation

Every original inertia element is determined by its actual intrinsic finite-normalization restrictions.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w

Lean source · statement

theorem actualFiniteInertiaRestriction_jointly_injective
    (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).carrier)
    (σ τ : (actualNormalizationInertiaGroup A K L Q).carrier)
    (h : ∀ E : FiniteGaloisIntermediateField K L,
      (actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ =
        (actualFiniteInertiaRestriction A K L Q E).hom'.toFun τ) : σ = τ

Module documentation

Actual finite inertia restrictions separate original inertia

Declarations

actualFiniteInertiaRestriction_jointly_injective