EtaleFundamentalGroups.Inertia.finiteNormalization_inertia_exists_native_lift
The proved field extension constructs a native original inertia element with exactly the given intrinsic coefficient RingHom.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageActionLean source · statement
theorem finiteNormalization_inertia_exists_native_lift
(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]
[IsGalois K F] [FiniteDimensional K F]
(Q : Ideal (normalizationCommAlgCat A F))
(τ : commAlgIdealInertiaGroup A (normalizationCommAlgCat A F) Q) :
∃ σ : actualNormalizationInertiaGroup A K F Q,
normalizationGaloisRingHom A K F (actualNormalizationInertiaElement A K F Q σ) =
commAlgIdealInertiaRingHom A (normalizationCommAlgCat A F) Q τ