AlgebraicGeometry.FiniteEtale.exists_constantCover_section_factorization
Every categorical section after a separable constant extension factors through the pullback of an actual finite étale constant cover.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtaleLean source · statement
theorem exists_constantCover_section_factorization
(k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsSeparable k L]
(X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
(f : X ⟶ Spec (.of k)) (Y : FiniteEtale X)
(s : ⊤_ (FiniteEtale (Limits.pullback
(Spec.map (CommRingCat.ofHom (algebraMap k L))) f)) ⟶
(pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)).obj Y) :
∃ A : FiniteEtale (Spec (.of k)), ∃ q : (pullback f).obj A ⟶ Y,
∃ r : ⊤_ (FiniteEtale (Limits.pullback
(Spec.map (CommRingCat.ofHom (algebraMap k L))) f)) ⟶
(pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)).obj
((pullback f).obj A),
r ≫ (pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)).map q = s