Module

FundamentalGroup.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.FundamentalGroup

12 declarations indexed from sourceView source ↗

Module documentation

Geometric fibers and field-valued points

This module identifies geometric fibers of finite étale schemes with morphisms from the field point and with algebra homomorphisms from their section rings.

Imports7

Nyll.EtaleFundamentalGroups.Pi1.FiniteEtale.GaloisCategory
Nyll.EtaleFundamentalGroups.Pi1.GeometricFiber.FieldPoints
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.FieldTheory.Galois.Profinite
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Nyll.SchemeTheory.Pi1.FiniteEtale.Geometry

Imported by31

def

fiberObjEquivHom

L60 ↗

AlgebraicGeometry.FiniteEtale.fiberObjEquivHom

Documentation

Identify points of the finite etale fiber with morphisms from the field point in the over category.

Source context 6 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)

Lean source · statement

def fiberObjEquivHom (X : FiniteEtale S) : (fiber «ξ»).obj X ≃ (Over.mk «ξ» ⟶ X.toComma)

lemma

fiberObjEquivHom_symm_naturality

L152 ↗

AlgebraicGeometry.FiniteEtale.fiberObjEquivHom_symm_naturality

Source context 6 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)

Lean source · statement

lemma fiberObjEquivHom_symm_naturality {X Y : FiniteEtale S} (f : X ⟶ Y) (x) :
    (fiber «ξ»).map f ((fiberObjEquivHom «ξ» X).symm x) =
      (fiberObjEquivHom «ξ» Y).symm (x ≫ f.hom)

lemma

fiberObjEquivHom_naturality

L264 ↗

AlgebraicGeometry.FiniteEtale.fiberObjEquivHom_naturality

Source context 6 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)

Lean source · statement

lemma fiberObjEquivHom_naturality {X Y : FiniteEtale S} (f : X ⟶ Y) (x) :
    (fiberObjEquivHom «ξ» X x) ≫ f.hom = fiberObjEquivHom «ξ» Y ((fiber «ξ»).map f x)

def

fiberIsoCoyoneda

L274 ↗

AlgebraicGeometry.FiniteEtale.fiberIsoCoyoneda

Documentation

The natural identification of the fiber functor with morphisms from the field point in the over category.

Source context 6 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)

Lean source · statement

def fiberIsoCoyoneda :
    fiber «ξ» ⋙ CategoryTheory.forget FintypeCat ≅ forget _ ⋙ coyoneda.obj ⟨Over.mk «ξ»⟩

instance

(anonymous instance)

L287 ↗

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · full declaration

instance (X : FiniteEtale (Spec (.of k))) [IsSepClosed K] :
    MulAction (K ≃ₐ[k] K) ((fib k K).obj X) where
  smul g x :=
    (fiberIsoCoyoneda (ξ k K)).inv.app X
      (g • (fiberIsoCoyoneda (ξ k K)).hom.app X x)
  one_smul x := by
    change (fiberObjEquivHom (ξ k K) X).symm
      (1 • fiberObjEquivHom (ξ k K) X x) = x
    have hOne : (1 : K ≃ₐ[k] K) • fiberObjEquivHom (ξ k K) X x =
        fiberObjEquivHom (ξ k K) X x :=
      one_smul (K ≃ₐ[k] K) _
    exact (congrArg (fiberObjEquivHom (ξ k K) X).symm hOne).trans
      (Equiv.symm_apply_apply _ _)
  mul_smul g h x := by
    change (fiberObjEquivHom (ξ k K) X).symm
        ((g * h) • fiberObjEquivHom (ξ k K) X x) =
      (fiberObjEquivHom (ξ k K) X).symm
        (g • fiberObjEquivHom (ξ k K) X
          ((fiberObjEquivHom (ξ k K) X).symm
            (h • fiberObjEquivHom (ξ k K) X x)))
    rw [Equiv.apply_symm_apply, mul_smul]

lemma

algEquiv_smul_fiber_def

L309 ↗

AlgebraicGeometry.FiniteEtale.algEquiv_smul_fiber_def

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

lemma algEquiv_smul_fiber_def [IsSepClosed K] (g : K ≃ₐ[k] K) (x : (fib k K).obj X) :
    g • x = (fiberObjEquivHom (ξ k K) X).symm (g • ((fiberObjEquivHom (ξ k K) X) x))

lemma

isField_of_isConnected

L313 ↗

AlgebraicGeometry.FiniteEtale.isField_of_isConnected

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

lemma isField_of_isConnected (X : FiniteEtale (Spec (.of k))) [IsConnected X] :
    IsField Γ(X.left, ⊤)

instance

(anonymous instance)

L403 ↗

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

instance (X : FiniteEtale (Spec (.of k))) [IsConnected X] : Field Γ(X.left, ⊤)

instance

(anonymous instance)

L407 ↗

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

instance : ContinuousSMul (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma)

instance

isGalois_of_isGalois

L437 ↗

AlgebraicGeometry.FiniteEtale.isGalois_of_isGalois

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

instance isGalois_of_isGalois (X : FiniteEtale (Spec (.of k))) [IsGalois X] :
    IsGalois k Γ(X.left, ⊤)

instance

(anonymous instance)

L491 ↗

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

instance [IsGalois k K] (X : FiniteEtale (Spec (.of k))) [IsGalois X] :
    MulAction.IsPretransitive (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma)

instance

(anonymous instance)

L507 ↗

Source context 10 commands

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

@[expose] public section
universe u
open CategoryTheory PreGaloisCategory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  («ξ» : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))
attribute [local instance] IsSepClosure.sep_closed
variable [IsSepClosure k K]

Lean source · full declaration

instance : IsFundamentalGroup (fib k K) (K ≃ₐ[k] K) where
  naturality g X Y f x := by
    apply (fiberObjEquivHom (ξ k K) Y).injective
    rw [algEquiv_smul_fiber_def, algEquiv_smul_fiber_def]
    simp only [fiberObjEquivHom_symm_naturality, Equiv.apply_symm_apply]
    rw [← fiberObjEquivHom_naturality (ξ k K) f x]
    ext1
    simp only [algEquiv_smul_hom]
    exact Category.assoc _ _ _
  continuous_smul X := by
    rw [continuousSMul_iff_stabilizer_isOpen]
    intro x
    let e := fiberObjEquivHom (ξ k K) X
    let : DiscreteTopology (Over.mk (ξ k K) ⟶ X.toComma) :=
      discreteTopology_bot _
    have hopen := stabilizer_isOpen (K ≃ₐ[k] K) (e x)
    convert hopen using 1
    ext g
    change (g • x = x) ↔ (g • e x = e x)
    rw [algEquiv_smul_fiber_def]
    constructor
    · intro h
      simpa only [e, Equiv.apply_symm_apply] using congrArg e h
    · intro h
      apply e.injective
      simpa only [e, Equiv.apply_symm_apply] using h
  transitive_of_isGalois X _ := by
    constructor
    intro x y
    obtain ⟨g, hg⟩ := MulAction.exists_smul_eq (K ≃ₐ[k] K)
      (fiberObjEquivHom _ _ x) (fiberObjEquivHom _ _ y)
    use g
    rw [algEquiv_smul_fiber_def]
    apply (fiberObjEquivHom (ξ k K) X).injective
    simp [hg]
  non_trivial' g H := by
    refine eq_one_of_smul_eq (k := k) (K := K) g ?_
    intro X x
    apply (fiberObjEquivHom (ξ k K) X).symm.injective
    specialize H X ((fiberObjEquivHom (ξ k K) X).symm x)
    rwa [algEquiv_smul_fiber_def, Equiv.apply_symm_apply] at H

Module documentation

Geometric fibers and field-valued points

Declarations