Module

FiniteGaloisSets.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.FiniteGaloisSets

1 declaration indexed from sourceView source ↗

Module documentation

Finite Galois sets over a field

This file supplies the finite part of the equivalence in Stacks Project, Tag 03QR. It directly transports the canonical Galois-category equivalence along the canonical topological group isomorphism from the absolute Galois group to the automorphism group of the geometric fiber functor.

Imports2

Mathlib.CategoryTheory.Galois.Equivalence
Nyll.EtaleFundamentalGroups.GeometricFiber.FundamentalGroup

Imported by4

def

equivContAction

L37 ↗

AlgebraicGeometry.FiniteEtale.equivContAction

Documentation

Finite étale k-schemes are canonically equivalent to finite continuous sets with an action of the absolute Galois group of k. This is the finite part of Stacks Project, Tag 03QR.

Source context 7 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]

Lean source · statement

def equivContAction :
    FiniteEtale (Spec (.of k)) ≌ ContAction FintypeCat.{u} (K ≃ₐ[k] K)

Module documentation

Finite Galois sets over a field

Declarations

equivContAction