NYLL
Module

ContinuousGaloisSet.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ContinuousGaloisSet
7 declarations indexed from sourceView source ↗

Module documentation

The geometric fiber as a continuous Galois set

This file constructs the forward functor in Stacks Project, Tag 03QR. For a separable closure K/k, an étale k-scheme is sent to its set of geometric points, with the discrete topology and the natural continuous action of K ≃ₐ[k] K by precomposition.

Imports3
Imported by2

Declarations

instance

geometricFiberMulAction

L37 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberMulAction
Documentation

The Galois action on geometric points is precomposition by the corresponding automorphism of Spec K.

Source context 7 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty
open scoped AlgebraicGeometry.FiniteEtale
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
Lean source · full declaration
instance geometricFiberMulAction
    (X : (Spec (.of k)).Etale) :
    MulAction (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma) where
  smul g x := by
    let σ : (Over.mk (ξ k K)).left ⟶ (Over.mk (ξ k K)).left := by
      change Spec (.of K) ⟶ Spec (.of K)
      exact Spec.map (CommRingCat.ofHom (g : K →+* K))
    let σOver : Over.mk (ξ k K) ⟶ Over.mk (ξ k K) :=
      Over.homMk σ (by
        change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ ξ k K = ξ k K
        rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← AlgEquiv.toAlgHom_toRingHom,
          AlgHom.comp_algebraMap])
    exact σOver ≫ x
  one_smul x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((1 : K ≃ₐ[k] K) : K →+* K)) ≫ x.left = x.left
    simp [AlgEquiv.aut_one]
  mul_smul g h x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((g * h : K ≃ₐ[k] K) : K →+* K)) ≫ x.left =
      Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫
        Spec.map (CommRingCat.ofHom (h : K →+* K)) ≫ x.left
    simp [AlgEquiv.aut_mul, Category.assoc]
lemma

geometricFiber_smul_left

L63 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiber_smul_left
Source context 9 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty
open scoped AlgebraicGeometry.FiniteEtale
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
/-- The Galois action on geometric points is precomposition by the
corresponding automorphism of `Spec K`. -/
local instance geometricFiberMulAction
    (X : (Spec (.of k)).Etale) :
    MulAction (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma) where
  smul g x := by
    let σ : (Over.mk (ξ k K)).left ⟶ (Over.mk (ξ k K)).left := by
      change Spec (.of K) ⟶ Spec (.of K)
      exact Spec.map (CommRingCat.ofHom (g : K →+* K))
    let σOver : Over.mk (ξ k K) ⟶ Over.mk (ξ k K) :=
      Over.homMk σ (by
        change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ ξ k K = ξ k K
        rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← AlgEquiv.toAlgHom_toRingHom,
          AlgHom.comp_algebraMap])
    exact σOver ≫ x
  one_smul x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((1 : K ≃ₐ[k] K) : K →+* K)) ≫ x.left = x.left
    simp [AlgEquiv.aut_one]
  mul_smul g h x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((g * h : K ≃ₐ[k] K) : K →+* K)) ≫ x.left =
      Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫
        Spec.map (CommRingCat.ofHom (h : K →+* K)) ≫ x.left
    simp [AlgEquiv.aut_mul, Category.assoc]
omit [IsSepClosure k K] in
Lean source · statement
lemma geometricFiber_smul_left (X : (Spec (.of k)).Etale)
    (g : K ≃ₐ[k] K) (x : Over.mk (ξ k K) ⟶ X.toComma) :
    (g • x).left = Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ x.left
instance

geometricFiberTopologicalSpace

L69 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberTopologicalSpace
Documentation

Geometric fibers are given the discrete topology.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty
open scoped AlgebraicGeometry.FiniteEtale
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
/-- The Galois action on geometric points is precomposition by the
corresponding automorphism of `Spec K`. -/
local instance geometricFiberMulAction
    (X : (Spec (.of k)).Etale) :
    MulAction (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma) where
  smul g x := by
    let σ : (Over.mk (ξ k K)).left ⟶ (Over.mk (ξ k K)).left := by
      change Spec (.of K) ⟶ Spec (.of K)
      exact Spec.map (CommRingCat.ofHom (g : K →+* K))
    let σOver : Over.mk (ξ k K) ⟶ Over.mk (ξ k K) :=
      Over.homMk σ (by
        change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ ξ k K = ξ k K
        rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← AlgEquiv.toAlgHom_toRingHom,
          AlgHom.comp_algebraMap])
    exact σOver ≫ x
  one_smul x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((1 : K ≃ₐ[k] K) : K →+* K)) ≫ x.left = x.left
    simp [AlgEquiv.aut_one]
  mul_smul g h x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((g * h : K ≃ₐ[k] K) : K →+* K)) ≫ x.left =
      Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫
        Spec.map (CommRingCat.ofHom (h : K →+* K)) ≫ x.left
    simp [AlgEquiv.aut_mul, Category.assoc]
Lean source · statement
instance geometricFiberTopologicalSpace (X : (Spec (.of k)).Etale) :
    TopologicalSpace (Over.mk (ξ k K) ⟶ X.toComma)
instance

geometricFiberDiscreteTopology

L73 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberDiscreteTopology
Source context 9 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty
open scoped AlgebraicGeometry.FiniteEtale
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
/-- The Galois action on geometric points is precomposition by the
corresponding automorphism of `Spec K`. -/
local instance geometricFiberMulAction
    (X : (Spec (.of k)).Etale) :
    MulAction (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma) where
  smul g x := by
    let σ : (Over.mk (ξ k K)).left ⟶ (Over.mk (ξ k K)).left := by
      change Spec (.of K) ⟶ Spec (.of K)
      exact Spec.map (CommRingCat.ofHom (g : K →+* K))
    let σOver : Over.mk (ξ k K) ⟶ Over.mk (ξ k K) :=
      Over.homMk σ (by
        change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ ξ k K = ξ k K
        rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← AlgEquiv.toAlgHom_toRingHom,
          AlgHom.comp_algebraMap])
    exact σOver ≫ x
  one_smul x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((1 : K ≃ₐ[k] K) : K →+* K)) ≫ x.left = x.left
    simp [AlgEquiv.aut_one]
  mul_smul g h x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((g * h : K ≃ₐ[k] K) : K →+* K)) ≫ x.left =
      Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫
        Spec.map (CommRingCat.ofHom (h : K →+* K)) ≫ x.left
    simp [AlgEquiv.aut_mul, Category.assoc]
/-- Geometric fibers are given the discrete topology. -/
local instance geometricFiberTopologicalSpace (X : (Spec (.of k)).Etale) :
    TopologicalSpace (Over.mk (ξ k K) ⟶ X.toComma) :=
  ⊥
Lean source · statement
instance geometricFiberDiscreteTopology (X : (Spec (.of k)).Etale) :
    DiscreteTopology (Over.mk (ξ k K) ⟶ X.toComma)
lemma

exists_finiteEtale_factorization

L80 ↗
AlgebraicGeometry.Scheme.Etale.exists_finiteEtale_factorization
Documentation

A geometric point of an étale scheme over a field factors through one finite étale component of the decomposition in Tag 02GL.

Source context 11 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty
open scoped AlgebraicGeometry.FiniteEtale
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
/-- The Galois action on geometric points is precomposition by the
corresponding automorphism of `Spec K`. -/
local instance geometricFiberMulAction
    (X : (Spec (.of k)).Etale) :
    MulAction (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma) where
  smul g x := by
    let σ : (Over.mk (ξ k K)).left ⟶ (Over.mk (ξ k K)).left := by
      change Spec (.of K) ⟶ Spec (.of K)
      exact Spec.map (CommRingCat.ofHom (g : K →+* K))
    let σOver : Over.mk (ξ k K) ⟶ Over.mk (ξ k K) :=
      Over.homMk σ (by
        change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ ξ k K = ξ k K
        rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← AlgEquiv.toAlgHom_toRingHom,
          AlgHom.comp_algebraMap])
    exact σOver ≫ x
  one_smul x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((1 : K ≃ₐ[k] K) : K →+* K)) ≫ x.left = x.left
    simp [AlgEquiv.aut_one]
  mul_smul g h x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((g * h : K ≃ₐ[k] K) : K →+* K)) ≫ x.left =
      Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫
        Spec.map (CommRingCat.ofHom (h : K →+* K)) ≫ x.left
    simp [AlgEquiv.aut_mul, Category.assoc]
/-- Geometric fibers are given the discrete topology. -/
local instance geometricFiberTopologicalSpace (X : (Spec (.of k)).Etale) :
    TopologicalSpace (Over.mk (ξ k K) ⟶ X.toComma) :=
  ⊥
local instance geometricFiberDiscreteTopology (X : (Spec (.of k)).Etale) :
    DiscreteTopology (Over.mk (ξ k K) ⟶ X.toComma) :=
  discreteTopology_bot _
omit [IsSepClosure k K] in
Lean source · statement
lemma exists_finiteEtale_factorization
    (X : (Spec (.of k)).Etale)
    (x : Over.mk (ξ k K) ⟶ X.toComma) :
    ∃ (Y : AlgebraicGeometry.FiniteEtale (Spec (.of k)))
      (f : Y.toComma ⟶ X.toComma)
      (y : Over.mk (ξ k K) ⟶ Y.toComma),
      y ≫ f = x
instance

geometricFiberContinuousSMul

L169 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberContinuousSMul
Documentation

The action on the geometric fiber of an arbitrary étale scheme is continuous. Openness is reduced to the finite component through which the chosen geometric point factors.

Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty
open scoped AlgebraicGeometry.FiniteEtale
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
/-- The Galois action on geometric points is precomposition by the
corresponding automorphism of `Spec K`. -/
local instance geometricFiberMulAction
    (X : (Spec (.of k)).Etale) :
    MulAction (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma) where
  smul g x := by
    let σ : (Over.mk (ξ k K)).left ⟶ (Over.mk (ξ k K)).left := by
      change Spec (.of K) ⟶ Spec (.of K)
      exact Spec.map (CommRingCat.ofHom (g : K →+* K))
    let σOver : Over.mk (ξ k K) ⟶ Over.mk (ξ k K) :=
      Over.homMk σ (by
        change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ ξ k K = ξ k K
        rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← AlgEquiv.toAlgHom_toRingHom,
          AlgHom.comp_algebraMap])
    exact σOver ≫ x
  one_smul x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((1 : K ≃ₐ[k] K) : K →+* K)) ≫ x.left = x.left
    simp [AlgEquiv.aut_one]
  mul_smul g h x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((g * h : K ≃ₐ[k] K) : K →+* K)) ≫ x.left =
      Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫
        Spec.map (CommRingCat.ofHom (h : K →+* K)) ≫ x.left
    simp [AlgEquiv.aut_mul, Category.assoc]
/-- Geometric fibers are given the discrete topology. -/
local instance geometricFiberTopologicalSpace (X : (Spec (.of k)).Etale) :
    TopologicalSpace (Over.mk (ξ k K) ⟶ X.toComma) :=
  ⊥
local instance geometricFiberDiscreteTopology (X : (Spec (.of k)).Etale) :
    DiscreteTopology (Over.mk (ξ k K) ⟶ X.toComma) :=
  discreteTopology_bot _
Lean source · statement
instance geometricFiberContinuousSMul (X : (Spec (.of k)).Etale) :
    ContinuousSMul (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma)
def

geometricFiber

L198 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiber
Documentation

The forward functor in Tag 03QR: an étale k-scheme is sent to its discrete continuous set of K-valued geometric points.

Source context 11 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty
open scoped AlgebraicGeometry.FiniteEtale
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
/-- The Galois action on geometric points is precomposition by the
corresponding automorphism of `Spec K`. -/
local instance geometricFiberMulAction
    (X : (Spec (.of k)).Etale) :
    MulAction (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma) where
  smul g x := by
    let σ : (Over.mk (ξ k K)).left ⟶ (Over.mk (ξ k K)).left := by
      change Spec (.of K) ⟶ Spec (.of K)
      exact Spec.map (CommRingCat.ofHom (g : K →+* K))
    let σOver : Over.mk (ξ k K) ⟶ Over.mk (ξ k K) :=
      Over.homMk σ (by
        change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ ξ k K = ξ k K
        rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← AlgEquiv.toAlgHom_toRingHom,
          AlgHom.comp_algebraMap])
    exact σOver ≫ x
  one_smul x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((1 : K ≃ₐ[k] K) : K →+* K)) ≫ x.left = x.left
    simp [AlgEquiv.aut_one]
  mul_smul g h x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((g * h : K ≃ₐ[k] K) : K →+* K)) ≫ x.left =
      Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫
        Spec.map (CommRingCat.ofHom (h : K →+* K)) ≫ x.left
    simp [AlgEquiv.aut_mul, Category.assoc]
/-- Geometric fibers are given the discrete topology. -/
local instance geometricFiberTopologicalSpace (X : (Spec (.of k)).Etale) :
    TopologicalSpace (Over.mk (ξ k K) ⟶ X.toComma) :=
  ⊥
local instance geometricFiberDiscreteTopology (X : (Spec (.of k)).Etale) :
    DiscreteTopology (Over.mk (ξ k K) ⟶ X.toComma) :=
  discreteTopology_bot _
/-- The action on the geometric fiber of an arbitrary étale scheme is
continuous.  Openness is reduced to the finite component through which the
chosen geometric point factors. -/
local instance geometricFiberContinuousSMul (X : (Spec (.of k)).Etale) :
    ContinuousSMul (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma) := by
  rw [continuousSMul_iff_stabilizer_isOpen]
  intro x
  obtain ⟨Y, f, y, hy⟩ := exists_finiteEtale_factorization k K X x
  rw [← hy]
  let : TopologicalSpace (Over.mk (ξ k K) ⟶ Y.toComma) := ⊥
  let : DiscreteTopology (Over.mk (ξ k K) ⟶ Y.toComma) :=
    discreteTopology_bot _
  have hyContinuous :
      ContinuousSMul (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ Y.toComma) :=
    inferInstance
  have hyOpen :
      IsOpen (MulAction.stabilizer (K ≃ₐ[k] K) y : Set (K ≃ₐ[k] K)) :=
    (continuousSMul_iff_stabilizer_isOpen.mp hyContinuous) y
  apply Subgroup.isOpen_mono
    (H₁ := MulAction.stabilizer (K ≃ₐ[k] K) y) ?_ hyOpen
  intro g hg
  rw [MulAction.mem_stabilizer_iff] at hg ⊢
  have hgLeft := congrArg (fun z ↦ z.left) hg
  change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ y.left = y.left at hgLeft
  ext1
  change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫
      (y.left ≫ f.left) = y.left ≫ f.left
  rw [← Category.assoc, hgLeft]
Lean source · statement
def geometricFiber :
    (Spec (.of k)).Etale ⥤ DiscreteContAction TopCat (K ≃ₐ[k] K)

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