NYLL
Module

SchemeHomDescent.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.SchemeHomDescent
3 declarations indexed from sourceView source ↗

Module documentation

Descent of scheme morphisms to a finite constant field

For a qcqs scheme over a field, a morphism from an algebraic constant extension to a fixed locally finitely presented scheme descends to an actual finite intermediate field. The structure map and recovery equality use the native constant-field pullbacks.

Imports3
Imported by3

Declarations

theorem

exists_finiteIntermediateField_schemeHom

L31 ↗
EtaleFundamentalGroups.exists_finiteIntermediateField_schemeHom
Documentation

An X-morphism from X_L to a locally finitely presented X-scheme descends to a finite intermediate field of an algebraic extension L/k.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
Lean source · statement
theorem exists_finiteIntermediateField_schemeHom
    [Algebra.IsAlgebraic k L]
    (X Y : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k)) (h : Y ⟶ X)
    [CompactSpace X] [QuasiSeparatedSpace X] [LocallyOfFinitePresentation h]
    (a : pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f ⟶ Y)
    (ha : a ≫ h = pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    ∃ s : Finset L, FiniteDimensional k (IntermediateField.adjoin k (s : Set L)) ∧
      ∃ g : pullback (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f ⟶ Y,
        (constantFieldInverseLimitCone k L X f).π.app (op s) ≫ g = a ∧
        g ≫ h = pullback.snd (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f
theorem

exists_constantFieldStage_hom_eq

L63 ↗
EtaleFundamentalGroups.exists_constantFieldStage_hom_eq
Documentation

Two maps from finite coefficient stages which agree over the extension field already agree over an actual common finite coefficient stage.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
Lean source · statement
theorem exists_constantFieldStage_hom_eq
    (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k)) [CompactSpace X]
    {Y : Scheme.{u}} (h : Y ⟶ X) [LocallyOfFiniteType h]
    (s r : Finset L)
    (a : pullback (Spec.map (CommRingCat.ofHom
      (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f ⟶ Y)
    (b : pullback (Spec.map (CommRingCat.ofHom
      (algebraMap k (IntermediateField.adjoin k (r : Set L))))) f ⟶ Y)
    (ha : a ≫ h = pullback.snd (Spec.map (CommRingCat.ofHom
      (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
    (hb : b ≫ h = pullback.snd (Spec.map (CommRingCat.ofHom
      (algebraMap k (IntermediateField.adjoin k (r : Set L))))) f)
    (hab : (constantFieldInverseLimitCone k L X f).π.app (op s) ≫ a =
      (constantFieldInverseLimitCone k L X f).π.app (op r) ≫ b) :
    ∃ (t : Finset L) (hst : s ⊆ t) (hrt : r ⊆ t),
      (constantFieldInverseLimitDiagram k L X f).map (homOfLE hst).op ≫ a =
        (constantFieldInverseLimitDiagram k L X f).map (homOfLE hrt).op ≫ b
theorem

exists_constantFieldStage_hom_eq_family

L98 ↗
EtaleFundamentalGroups.exists_constantFieldStage_hom_eq_family
Documentation

A finite family of equalities over the extension holds simultaneously at one actual coefficient stage, including when the family is empty.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
Lean source · statement
theorem exists_constantFieldStage_hom_eq_family
    {ι : Type v} [Finite ι]
    (X Y : ι → Scheme.{u}) (f : ∀ i, X i ⟶ Spec (CommRingCat.of k))
    [∀ i, CompactSpace (X i)] (h : ∀ i, Y i ⟶ X i)
    [∀ i, LocallyOfFiniteType (h i)] (s : Finset L)
    (a b : ∀ i, (constantFieldInverseLimitDiagram k L (X i) (f i)).obj (op s) ⟶ Y i)
    (ha : ∀ i, a i ≫ h i = (constantFieldInverseLimitProjection k L (X i) (f i)).app (op s))
    (hb : ∀ i, b i ≫ h i = (constantFieldInverseLimitProjection k L (X i) (f i)).app (op s))
    (hab : ∀ i, (constantFieldInverseLimitCone k L (X i) (f i)).π.app (op s) ≫ a i =
      (constantFieldInverseLimitCone k L (X i) (f i)).π.app (op s) ≫ b i) :
    ∃ (t : Finset L) (hst : s ⊆ t), ∀ i,
      (constantFieldInverseLimitDiagram k L (X i) (f i)).map (homOfLE hst).op ≫ a i =
        (constantFieldInverseLimitDiagram k L (X i) (f i)).map (homOfLE hst).op ≫ b i

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.