Module

ActualFiniteNormalizationTowerFaithful.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteNormalizationTowerFaithful

1 declaration indexed from sourceView source ↗

Module documentation

Faithfulness of finite normalization restriction

An ambient automorphism fixing a larger finite normalization fixes every smaller finite normalization. The actual coefficient square and the literal injective normalization inclusion supply the implication.

Imports4

Imported by3

theorem

actualFiniteNormalizationRestrictionRingHom_eq_id_of_tower

L28 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationRestrictionRingHom_eq_id_of_tower

Documentation

Trivial action on a finite normalization descends through its literal injective inclusion from any 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 actualFiniteNormalizationRestrictionRingHom_eq_id_of_tower
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) (σ : Gal(L/K))
    (hσ : actualFiniteNormalizationRestrictionRingHom A K L F σ =
      RingHom.id (finiteAbsoluteNormalizationAlgebra A K L F).carrier) :
    actualFiniteNormalizationRestrictionRingHom A K L E σ =
      RingHom.id (finiteAbsoluteNormalizationAlgebra A K L E).carrier

Module documentation

Faithfulness of finite normalization restriction

Declarations

actualFiniteNormalizationRestrictionRingHom_eq_id_of_tower