AlgebraicGeometry.FiniteEtale.existsUnique_section_of_fixed_point
A fixed point of the actual geometric fiber determines a unique section of the original finite étale cover with the specified geometric value.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X]
{Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)Lean source · statement
theorem existsUnique_section_of_fixed_point
(W : FiniteEtale X) (z : Spec (.of Ω) ⟶ W.left) (hz : z ≫ W.hom = xi)
(hfixed : ∀ g : Aut (fiber xi), g •
((fiberObjEquivHom xi W).symm (Over.homMk z hz)) =
(fiberObjEquivHom xi W).symm (Over.homMk z hz)) :
∃! s : X ⟶ W.left, s ≫ W.hom = 𝟙 X ∧ xi ≫ s = z