EtaleFundamentalGroups.fieldFiniteEtaleCoverCompositePoint
The canonical field-cover point expressed at the literal composite geometric point Spec Omega → Spec F → Spec K.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L Omega F : Type u)
variable [Field K] [Field L] [Field Omega] [Field F]
variable [Algebra K L] [FiniteDimensional K L] [_root_.IsGalois K L]
variable [Algebra K Omega] [Algebra L Omega] [IsScalarTower K L Omega]
variable [IsSepClosed Omega]
variable [Algebra K F] [Algebra F Omega] [IsScalarTower K F Omega]Lean source · statement
def fieldFiniteEtaleCoverCompositePoint :
(fiber (ξ F Omega ≫ ξ K F)).obj (FiniteEtale.mk (ξ K L))