EtaleFundamentalGroups.Inertia.etale_normalization_of_galoisComponents
Étaleness of every pointed normalized Galois component implies étaleness of the actual normalization of the entire pulled-back cover.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.Inertia
universe uLean source · statement
theorem etale_normalization_of_galoisComponents
{U V S : Scheme.{u}} [ConnectedSpace U] [ConnectedSpace V]
(b : U ⟶ V) {Ω : Type u} [Field Ω] [IsSepClosed Ω]
(xi : Spec (.of Ω) ⟶ U) (W : FiniteEtale V) (hW : IsGalois W)
(f : ((FiniteEtale.pullback b).obj W).left ⟶ S)
[QuasiCompact f] [QuasiSeparated f]
(hcomponent : ∀ (w : (fiber (xi ≫ b)).obj W)
(Z : FiniteEtale U) (i : Z ⟶ (FiniteEtale.pullback b).obj W)
(v : (fiber xi).obj Z),
(fiber xi).map i v = transportedPointOfCompIso (FiniteEtale.pullback b)
(pullbackFiberIso b xi) W w →
IsGalois Z → Mono i → Etale (i.left ≫ f).fromNormalization) :
Etale f.fromNormalization