AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_field_fiberLift
The actual induced fundamental-group action is the original field Galois automorphism acting on the geometric lift by precomposition.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
attribute [local instance] IsSepClosure.sep_closed
variable {k Ω : Type u} [Field k] [Field Ω] [Algebra k Ω] [IsSepClosure k Ω]
{X : Scheme.{u}} (f : Spec (.of k) ⟶ X)Lean source · statement
theorem fundamentalGroupHom_field_fiberLift
(W : FiniteEtale X) (σ : Ω ≃ₐ[k] Ω)
(x : (fiber ((ξ k Ω) ≫ f)).obj W) :
(fiberObjEquivHom ((ξ k Ω) ≫ f) W
((fundamentalGroupHom f (ξ k Ω) (toAut (fib k Ω) (Ω ≃ₐ[k] Ω) σ)).hom.app W x)).left =
Spec.map (CommRingCat.ofHom (σ : Ω →+* Ω)) ≫
(fiberObjEquivHom ((ξ k Ω) ≫ f) W x).left