Module

ActualFiniteNormalizationInclusionSquare.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteNormalizationInclusionSquare

2 declarations indexed from sourceView source ↗

Module documentation

Finite normalization inclusion squares

Factors the finite ambient inclusion through the original normalization and proves compatibility of this inclusion with restricted Galois automorphisms.

Imports3

Imported by6

theorem

actualFiniteNormalizationAmbientRingHom_factor

L31 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationAmbientRingHom_factor

Documentation

The literal finite-normalization inclusion factors the ambient inclusion.

Source context 5 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] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
omit [IsFractionRing A K] [IsGalois K L] in

Lean source · statement

theorem actualFiniteNormalizationAmbientRingHom_factor (E : FiniteGaloisIntermediateField K L) :
    (normalizationAmbientRingHom A (CommAlgCat.of A L)).comp
        (finiteAbsoluteNormalizationRingMap A K L E) =
      actualFiniteNormalizationAmbientRingHom A K L E

theorem

actualFiniteNormalizationRestrictionRingHom_inclusion

L39 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationRestrictionRingHom_inclusion