AlgebraicGeometry.Scheme.ofArrows_mem_smallEtaleTopology_iff_geometricFiber_jointlySurjective
A family in the small étale site of a field is covering exactly when its maps on the fiber at a separably closed geometric point are jointly surjective.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u
noncomputable section
open CategoryTheory Opposite
namespace AlgebraicGeometry.SchemeLean source · statement
theorem ofArrows_mem_smallEtaleTopology_iff_geometricFiber_jointlySurjective
{k Ω : Type u} [Field k] [Field Ω] [IsSepClosed Ω]
(s : Spec (.of Ω) ⟶ Spec (.of k))
{W : (Spec (.of k)).Etale} {ι : Type*}
{Z : ι → (Spec (.of k)).Etale} (f : ∀ i, Z i ⟶ W) :
Sieve.ofArrows Z f ∈ smallEtaleTopology (Spec (.of k)) W ↔
Presieve.ofArrows Z f ∈
Types.jointlySurjectivePrecoverage.comap
(Etale.forget (Spec (.of k)) ⋙ coyoneda.obj (op (Over.mk s))) W