SchemeTheory.normalizationGaloisGroupMap_surjective
The prescribed native finite normalization group map is onto the intrinsic coefficient automorphism group. The actual fraction-extension producer constructs its preimages.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v wLean source · statement
theorem normalizationGaloisGroupMap_surjective
(A : Type u) (K : Type v) (F : Type w)
[CommRing A] [Field K] [Field F]
[Algebra A K] [IsFractionRing A K]
[Algebra K F] [Algebra A F] [IsScalarTower A K F]
[FiniteDimensional K F] :
Function.Surjective (normalizationGaloisGroupMap A K F).hom