AlgebraicGeometry.FiniteEtale.isGalois_over_intermediate
A connected finite étale Galois cover is Galois over every connected intermediate finite étale scheme.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
namespace AlgebraicGeometry.FiniteEtaleLean source · statement
theorem isGalois_over_intermediate
{S : Scheme.{u}} [ConnectedSpace S]
(A B : FiniteEtale S) [IsGalois A] [ConnectedSpace B.left]
(f : A ⟶ B) {Ω : Type u} [Field Ω] [IsSepClosed Ω]
(geom : Spec (.of Ω) ⟶ A.left) :
IsGalois (C := FiniteEtale B.left) (FiniteEtale.mk f.left)