AlgebraicGeometry.FiniteEtale.exists_intermediate_finiteEtale_of_deckSubgroup
A prescribed deck subgroup gives an actual connected intermediate scheme and an actual relative Galois cover with exactly that relative deck group.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
namespace AlgebraicGeometry.FiniteEtaleLean source · statement
theorem exists_intermediate_finiteEtale_of_deckSubgroup
{S : Scheme} [ConnectedSpace S] (A : FiniteEtale S) [IsGalois A]
{Ω : Type} [Field Ω] [IsSepClosed Ω]
(geom : Spec (.of Ω) ⟶ A.left) (H : Subgroup (Aut A)ᵐᵒᵖ) :
∃ (B : FiniteEtale S) (_ : ConnectedSpace B.left) (f : A ⟶ B),
IsGalois (C := FiniteEtale B.left) (FiniteEtale.mk f.left) ∧
(∀ σ : Aut A, σ.hom ≫ f = f ↔ MulOpposite.op σ ∈ H) ∧
(∀ τ : Aut (FiniteEtale.mk f.left), ∃ σ : Aut A,
σ.hom.left = τ.hom.left ∧ MulOpposite.op σ ∈ H)