Module

ActualFiniteDecompositionTowerKernel.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteDecompositionTowerKernel

2 declarations indexed from sourceView source ↗

Module documentation

Kernels of actual finite decomposition restrictions

The actual coefficient cancellation theorem shows that the kernel of the larger-stage restriction lies in the kernel of the smaller-stage restriction. No factor map or kernel inclusion is supplied as an assumption.

Imports8

Imported by2

theorem

actualFiniteDecompositionRestriction_eq_one_of_tower

L32 ↗

EtaleFundamentalGroups.Inertia.actualFiniteDecompositionRestriction_eq_one_of_tower

Documentation

Fixing the larger finite normalization forces an actual original decomposition element to fix every smaller finite normalization.

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 actualFiniteDecompositionRestriction_eq_one_of_tower
    (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)
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F)
    (σ : (normalizationDecompositionGroup A K L Q).carrier)
    (hσ : (actualFiniteDecompositionRestriction A K L Q F).hom'.toFun σ = 1) :
    (actualFiniteDecompositionRestriction A K L Q E).hom'.toFun σ = 1

theorem

actualFiniteDecompositionRestriction_ker_le_of_tower

L57 ↗

EtaleFundamentalGroups.Inertia.actualFiniteDecompositionRestriction_ker_le_of_tower