EtaleFundamentalGroups.Inertia.finiteAbsoluteNormalizationAutomorphisms_finite
Finiteness of the intrinsic coefficient automorphisms of an actual finite normalization, proved before introducing any original prime or inertia.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
universe u v wLean source · statement
theorem finiteAbsoluteNormalizationAutomorphisms_finite
(A : Type u) (K : Type v) (L : Type w)
[CommRing A] [IsDedekindDomain A] [Field K] [Field L]
[Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
(E : FiniteGaloisIntermediateField K L) :
Finite (finiteAbsoluteNormalizationAlgebra A K L E ≃ₐ[A]
finiteAbsoluteNormalizationAlgebra A K L E)