Module

GaloisCategory.lean

Nyll.EtaleFundamentalGroups.Pi1.FiniteEtale.GaloisCategory

10 declarations indexed from sourceView source ↗

Module documentation

The category of finite étale morphisms over a connected base is a Galois category

Let S be a scheme and denote by FEt S the category of finite étale schemes over S. Then FEt S is a PreGaloisCategory.

Imports4

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Nyll.SchemeTheory.Pi1.FiniteEtale.Geometry

Imported by19

instance

(anonymous instance)

L36 ↗

Source context 4 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits

Lean source · statement

instance {C : Type*} [Category C] {G : Type*} [Group G] [Finite G] [HasFiniteColimits C] :
    HasColimitsOfShape (SingleObj G) C

instance

(anonymous instance)

L41 ↗

Source context 4 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits

Lean source · statement

instance {C D : Type*} [Category C] [Category D] (F : C ⥤ D) {G : Type*} [Group G] [Finite G]
    [PreservesFiniteColimits F] :
    PreservesColimitsOfShape (SingleObj G) F

instance

(anonymous instance)

L54 ↗

Documentation

The category of finite étale morphisms is a pre-galois category.

Source context 7 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})

Lean source · full declaration

instance (X : Scheme.{u}) : PreGaloisCategory (FiniteEtale X) where
  hasQuotientsByFiniteGroups G := inferInstance
  monoInducesIsoOnDirectSummand {f g} i hi := by
    let hfg : IsFiniteEtale g.hom := g.2
    let : IsFinite g.hom := hfg.toIsFinite
    let : Etale g.hom := hfg.toEtale
    rw [FiniteEtale.mono_iff] at hi
    obtain ⟨ho, hc⟩ := hi
    let : IsOpenImmersion i.hom.left := ho
    let : IsClosedImmersion i.hom.left := hc
    let A : Set g.left := Set.range i.hom.left.base
    have hA : IsClosed A := i.hom.left.isClosedEmbedding.isClosed_range
    let U : g.left.Opens := ⟨Aᶜ, hA.isOpen_compl⟩
    let hUo : IsOpenImmersion U.ι := by
      dsimp only [U]
      infer_instance
    let hUc : IsClosedImmersion U.ι := by
      apply IsClosedImmersion.of_isPreimmersion U.ι
      simp only [Scheme.Opens.range_ι, TopologicalSpace.Opens.coe_mk, isClosed_compl_iff, U, A]
      apply IsOpenImmersion.isOpen_range
    let hUf : IsFinite U.ι := inferInstance
    let hUe : Etale U.ι := inferInstance
    let : IsFinite (U.ι ≫ g.hom) :=
      MorphismProperty.comp_mem
        (W := (@IsFinite : MorphismProperty Scheme.{u})) U.ι g.hom hUf hfg.toIsFinite
    let _ : Etale U.ι := hUe
    let _ : Etale g.hom := hfg.toEtale
    let : Etale (U.ι ≫ g.hom) := inferInstance
    let hU : IsFiniteEtale (U.ι ≫ g.hom) := ⟨⟩
    let u : FiniteEtale X := ⟨Over.mk (U.ι ≫ g.hom), hU⟩
    refine ⟨u, MorphismProperty.Over.homMk U.ι, ⟨?_⟩⟩
    apply isColimitOfReflectsOfMapIsColimit (FiniteEtale.forget X)
    apply isColimitOfReflectsOfMapIsColimit (Over.forget X)
    simp only [Over.forget_map]
    apply Nonempty.some
    refine nonempty_isColimit_binaryCofanMk_of_isCompl
      i.hom.left U.ι ?_
    constructor
    · rw [disjoint_iff]
      ext x
      simp only [Scheme.Hom.coe_opensRange, U, A,
        TopologicalSpace.Opens.coe_inf, TopologicalSpace.Opens.coe_bot, Set.mem_inter_iff,
        Set.mem_range]
      constructor
      · rintro ⟨⟨y, hy⟩, ⟨z, hz⟩⟩
        exact (z.property ⟨y, hy.trans hz.symm⟩).elim
      · intro hx
        exact hx.elim
    · rw [codisjoint_iff]
      ext x
      simp only [Scheme.Hom.coe_opensRange, U, A,
        TopologicalSpace.Opens.coe_sup, TopologicalSpace.Opens.coe_top, Set.mem_union,
        Set.mem_range, Set.mem_univ, iff_true]
      by_cases h : ∃ y, (MorphismProperty.Comma.Hom.hom i).left y = x
      · exact Or.inl h
      · exact Or.inr ⟨⟨x, h⟩, rfl⟩

def

fiber

L116 ↗

AlgebraicGeometry.FiniteEtale.fiber

Documentation

Pull back finite etale schemes along the field point and take their finite sets of points.

Source context 9 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}

Lean source · statement

def fiber : FiniteEtale X ⥤ FintypeCat

def

fiberPt

L121 ↗

AlgebraicGeometry.FiniteEtale.fiberPt

Documentation

Project a point of a finite etale fiber to the underlying point of its source scheme.

Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
variable {ξ} in

Lean source · statement

def fiberPt {A : FiniteEtale X} (x : (fiber ξ).obj A) : A.left

instance

(anonymous instance)

L124 ↗

Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
variable {ξ} in

Lean source · statement

instance : PreservesFiniteLimits (pullback ξ)

instance

(anonymous instance)

L129 ↗

Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
variable {ξ} in

Lean source · statement

instance [ConnectedSpace X] [IsSepClosed Ω] : (fiber ξ).ReflectsIsomorphisms

instance

(anonymous instance)

L133 ↗

Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
variable {ξ} in

Lean source · statement

instance [IsSepClosed Ω] : PreservesFiniteColimits (fiber ξ)

instance

fiberFunctor

L141 ↗

AlgebraicGeometry.FiniteEtale.fiberFunctor

Documentation

If X is a connected scheme and ξ : Spec Ω ⟶ X is a geometric point, taking fibers over ξ is a fiber functor.

Source context 11 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
variable {ξ} in
open PreGaloisCategory

Lean source · full declaration

instance fiberFunctor [ConnectedSpace X] [IsSepClosed Ω] : FiberFunctor (fiber ξ) where
  preservesTerminalObjects := by dsimp [fiber]; infer_instance
  preservesPullbacks := by dsimp [fiber]; infer_instance
  preservesQuotientsByFiniteGroups _ _ := inferInstance

instance

galoisCategory

L148 ↗

AlgebraicGeometry.FiniteEtale.galoisCategory

Documentation

If X is a connected scheme, the category of finite étale schemes over X is a Galois category.

Source context 11 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
variable {ξ} in
open PreGaloisCategory

Lean source · full declaration

instance galoisCategory [ConnectedSpace X] : GaloisCategory (FiniteEtale X) where
  hasFiberFunctor := by
    have : Nonempty X := inferInstance
    let x : X := ‹Nonempty X›.some
    let k : Type u := X.residueField x
    let Ω : Type u := AlgebraicClosure k
    let ξ : Spec (.of Ω) ⟶ X :=
      Spec.map (CommRingCat.ofHom <| algebraMap k Ω) ≫ X.fromSpecResidueField x
    exact ⟨fiber ξ, inferInstance⟩

Module documentation

The category of finite étale morphisms over a connected base is a Galois category

Declarations