NYLL
Module

ArithmeticSections.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticSections
3 declarations indexed from sourceView source ↗

Module documentation

Arithmetic Sections

A section after a separable algebraic constant extension factors through an actual finite étale constant cover of the base.

Imports3
Imported by4

Declarations

theorem

exists_constantCover_factorization

L28 ↗
AlgebraicGeometry.FiniteEtale.exists_constantCover_factorization
Documentation

A section after a separable algebraic constant extension factors through an actual finite étale constant cover of the base.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_constantCover_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)
    (a : Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f ⟶ Y.left)
    (ha : a ≫ Y.hom = pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    ∃ A : FiniteEtale (Spec (.of k)), Nonempty A.left ∧
      ∃ q : (pullback f).obj A ⟶ Y,
      ∃ b : Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f ⟶
        ((pullback f).obj A).left,
        b ≫ q.left = a ∧ b ≫ ((pullback f).obj A).hom =
          pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f
theorem

exists_constantCover_epi_of_section

L60 ↗
AlgebraicGeometry.FiniteEtale.exists_constantCover_epi_of_section
Documentation

A connected finite étale cover with a section after a separable constant extension is dominated by a finite étale constant cover.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_constantCover_epi_of_section
    (k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsSeparable k L]
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X] [ConnectedSpace X]
    (f : X ⟶ Spec (.of k)) (Y : FiniteEtale X) [IsConnected Y]
    (a : Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f ⟶ Y.left)
    (ha : a ≫ Y.hom = pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    ∃ A : FiniteEtale (Spec (.of k)), ∃ q : (pullback f).obj A ⟶ Y, Epi q
theorem

exists_constantCover_epi_of_terminal_hom

L81 ↗
AlgebraicGeometry.FiniteEtale.exists_constantCover_epi_of_terminal_hom
Documentation

A connected cover that acquires a categorical section over the separable extension is an epimorphic image of a constant cover.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_constantCover_epi_of_terminal_hom
    (k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsSeparable k L]
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X] [ConnectedSpace X]
    (f : X ⟶ Spec (.of k)) (Y : FiniteEtale X) [IsConnected Y]
    (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, Epi q

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