NYLL
Module

SchemePairDescent.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.SchemePairDescent
6 declarations indexed from sourceView source ↗

Module documentation

Scheme Pair Descent

A morphism from a qcqs constant extension to a locally finitely presented constant extension descends to one finite coefficient field, with both structure maps and recovery preserved.

Imports7
Imported by4

Declarations

theorem

exists_finiteIntermediateField_schemePairHom

L31 ↗
EtaleFundamentalGroups.exists_finiteIntermediateField_schemePairHom
Documentation

A morphism from a qcqs constant extension to a locally finitely presented constant extension descends to one finite coefficient field, with both structure maps and recovery preserved.

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_schemePairHom
    [Algebra.IsAlgebraic k L]
    (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
    (A B : Scheme.{u}) (p : A ⟶ X) (q : B ⟶ X)
    [CompactSpace A] [QuasiSeparatedSpace A] [LocallyOfFinitePresentation q]
    (a : pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) (p ≫ f) ⟶
      pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) (q ≫ f))
    (haX : a ≫ pullback.snd _ (q ≫ f) ≫ q =
      pullback.snd _ (p ≫ f) ≫ p)
    (haL : a ≫ pullback.fst _ (q ≫ f) = pullback.fst _ (p ≫ 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))))) (p ≫ f) ⟶
        pullback (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s : Set L))))) (q ≫ f),
        g ≫ pullback.fst _ (q ≫ f) = pullback.fst _ (p ≫ f) ∧
        g ≫ pullback.snd _ (q ≫ f) ≫ q =
          pullback.snd _ (p ≫ f) ≫ p ∧
        (constantFieldInverseLimitCone k L A (p ≫ f)).π.app (op s) ≫ g =
          a ≫ (constantFieldInverseLimitCone k L B (q ≫ f)).π.app (op s)
theorem

constantFieldSpec_comp

L93 ↗
EtaleFundamentalGroups.constantFieldSpec_comp
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 constantFieldSpec_comp
    (s : Finset L) :
    Spec.map (CommRingCat.ofHom (IntermediateField.adjoin k (s : Set L)).val.toRingHom) ≫
      Spec.map (CommRingCat.ofHom
        (algebraMap k (IntermediateField.adjoin k (s : Set L)))) =
      Spec.map (CommRingCat.ofHom (algebraMap k L))
theorem

constantFieldInverseLimitCone_π_app_isPullback

L103 ↗
EtaleFundamentalGroups.constantFieldInverseLimitCone_π_app_isPullback
Documentation

Each constant-field cone map is the base change of the literal coefficient inclusion.

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 constantFieldInverseLimitCone_π_app_isPullback
    (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k)) (s : Finset L) :
    IsPullback ((constantFieldInverseLimitCone k L X f).π.app (op s))
      (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)
      (pullback.fst (Spec.map (CommRingCat.ofHom
        (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
      (Spec.map (CommRingCat.ofHom
        (IntermediateField.adjoin k (s : Set L)).val.toRingHom))
theorem

isIso_of_constantFieldStageHom

L133 ↗
EtaleFundamentalGroups.isIso_of_constantFieldStageHom
Documentation

A map between constant-field stages that recovers an isomorphism over the extension field is already an isomorphism, by faithfully flat descent.

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 isIso_of_constantFieldStageHom
    (X Y : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
    (g : Y ⟶ Spec (CommRingCat.of k)) (s : Finset L)
    (a : pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f ⟶
      pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) g) [IsIso a]
    (b : pullback (Spec.map (CommRingCat.ofHom
        (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f ⟶
      pullback (Spec.map (CommRingCat.ofHom
        (algebraMap k (IntermediateField.adjoin k (s : Set L))))) g)
    (ha : a ≫ pullback.fst _ g = pullback.fst _ f)
    (hb : b ≫ pullback.fst _ g = pullback.fst _ f)
    (hab : (constantFieldInverseLimitCone k L X f).π.app (op s) ≫ b =
      a ≫ (constantFieldInverseLimitCone k L Y g).π.app (op s)) : IsIso b
theorem

exists_finiteIntermediateField_schemePairIso

L182 ↗
EtaleFundamentalGroups.exists_finiteIntermediateField_schemePairIso
Documentation

An isomorphism between constant extensions of schemes descends to an actual finite intermediate field, preserving the base and coefficient structure maps.

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_schemePairIso
    [Algebra.IsAlgebraic k L]
    (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
    (A B : Scheme.{u}) (p : A ⟶ X) (q : B ⟶ X)
    [CompactSpace A] [QuasiSeparatedSpace A] [LocallyOfFinitePresentation q]
    (e : pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) (p ≫ f) ≅
      pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) (q ≫ f))
    (heX : e.hom ≫ pullback.snd _ (q ≫ f) ≫ q =
      pullback.snd _ (p ≫ f) ≫ p)
    (heL : e.hom ≫ pullback.fst _ (q ≫ f) = pullback.fst _ (p ≫ f)) :
    ∃ s : Finset L, FiniteDimensional k (IntermediateField.adjoin k (s : Set L)) ∧
      ∃ e₀ : pullback (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s : Set L))))) (p ≫ f) ≅
        pullback (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s : Set L))))) (q ≫ f),
        e₀.hom ≫ pullback.fst _ (q ≫ f) = pullback.fst _ (p ≫ f) ∧
        e₀.hom ≫ pullback.snd _ (q ≫ f) ≫ q =
          pullback.snd _ (p ≫ f) ≫ p ∧
        (constantFieldInverseLimitCone k L A (p ≫ f)).π.app (op s) ≫ e₀.hom =
          e.hom ≫ (constantFieldInverseLimitCone k L B (q ≫ f)).π.app (op s)
theorem

exists_finiteIntermediateField_schemePairHom_family

L210 ↗
EtaleFundamentalGroups.exists_finiteIntermediateField_schemePairHom_family
Documentation

A finite family of morphisms of constant-field extensions descends to one actual finite coefficient field, preserving the two structure maps and recovery.

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_schemePairHom_family
    [Algebra.IsAlgebraic k L] {ι : Type v} [Finite ι]
    (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
    (A B : ι → Scheme.{u}) (p : ∀ i : ι, A i ⟶ X) (q : ∀ i : ι, B i ⟶ X)
    [∀ i : ι, CompactSpace (A i)] [∀ i : ι, QuasiSeparatedSpace (A i)]
    [∀ i : ι, LocallyOfFinitePresentation (q i)]
    (a : ∀ i : ι, pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) (p i ≫ f) ⟶
      pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) (q i ≫ f))
    (haX : ∀ i : ι, a i ≫ pullback.snd _ (q i ≫ f) ≫ q i =
      pullback.snd _ (p i ≫ f) ≫ p i)
    (haL : ∀ i : ι, a i ≫ pullback.fst _ (q i ≫ f) = pullback.fst _ (p i ≫ f)) :
    ∃ s : Finset L, FiniteDimensional k (IntermediateField.adjoin k (s : Set L)) ∧
      ∃ g : ∀ i : ι, pullback (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s : Set L))))) (p i ≫ f) ⟶
        pullback (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s : Set L))))) (q i ≫ f),
        ∀ i : ι, g i ≫ pullback.fst _ (q i ≫ f) = pullback.fst _ (p i ≫ f) ∧
          g i ≫ pullback.snd _ (q i ≫ f) ≫ q i =
            pullback.snd _ (p i ≫ f) ≫ p i ∧
          (constantFieldInverseLimitCone k L (A i) (p i ≫ f)).π.app (op s) ≫ g i =
            a i ≫ (constantFieldInverseLimitCone k L (B i) (q i ≫ f)).π.app (op s)

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