Fullness of the actual geometric fiber action functor descends a fixed point to a section. No connectedness of the covering scheme is assumed.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {X : Scheme.{u}}
{Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)instance : IsFiniteEtale (𝟙 X)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {X : Scheme.{u}}
{Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)
local instance : IsFiniteEtale (𝟙 X) := by constructortheorem identityFiber_subsingleton :
Subsingleton ((fiber xi).obj (FiniteEtale.mk (𝟙 X)))A finite etale cover admits an actual section exactly when its actual geometric fiber has a fixed point under the fundamental group.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {X : Scheme.{u}}
{Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)
local instance : IsFiniteEtale (𝟙 X) := by constructor
variable [ConnectedSpace X]theorem exists_section_iff_exists_fiber_fixed (W : FiniteEtale X) :
(∃ s : X ⟶ W.left, s ≫ W.hom = 𝟙 X) ↔
∃ q : (fiber xi).obj W, ∀ g : Aut (fiber xi), g • q = q