NYLL
Module

Basic.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.Basic
10 declarations indexed from sourceView source ↗

Module documentation

Galois objects and Galois covers

This file supplies the abstract Galois-category part of the four equivalent characterizations of a finite étale Galois cover in Stacks Project, Section 58.7 (03SF). It uses the canonical mathlib notion CategoryTheory.PreGaloisCategory.IsGalois.

Imports2
Imported by8

Declarations

theorem

isGalois_iff_evaluation_bijective

L38 ↗
CategoryTheory.PreGaloisCategory.isGalois_iff_evaluation_bijective
Documentation

A connected object of a Galois category is Galois if and only if evaluation at one point identifies its automorphism group with its fiber. This is the simply-transitive formulation in Stacks Project, Section 58.7.

Source context 7 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
open Limits
Lean source · full declaration
theorem isGalois_iff_evaluation_bijective (X : C) [IsConnected X] (x : F.obj X) :
    IsGalois X ↔ Function.Bijective (fun σ : Aut X ↦ F.map σ.hom x) := by
  constructor
  · intro h
    let : IsGalois X := h
    exact evaluation_aut_bijective_of_isGalois F X x
  · intro h
    rw [isGalois_iff_pretransitive F X, MulAction.isPretransitive_iff_base x]
    exact h.surjective
theorem

isGalois_iff_card_aut_eq_card_fiber

L54 ↗
CategoryTheory.PreGaloisCategory.isGalois_iff_card_aut_eq_card_fiber
Documentation

A connected object of a Galois category is Galois if and only if the cardinality of its automorphism group equals the cardinality of its fiber. For a finite étale cover the latter cardinality is its degree.

Source context 8 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
open Limits
attribute [local instance] FintypeCat.fintype
Lean source · statement
theorem isGalois_iff_card_aut_eq_card_fiber (X : C) [IsConnected X] :
    IsGalois X ↔ Nat.card (Aut X) = Nat.card (F.obj X)
lemma

fiberBinaryProduct_ext

L69 ↗
CategoryTheory.PreGaloisCategory.fiberBinaryProduct_ext
Source context 8 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
open Limits
attribute [local instance] FintypeCat.fintype
Lean source · statement
lemma fiberBinaryProduct_ext {X Y : C} {a b : F.obj (X ⨯ Y)}
    (hfst : F.map prod.fst a = F.map prod.fst b)
    (hsnd : F.map prod.snd a = F.map prod.snd b) :
    a = b
theorem

isGalois_of_mono_to_binaryProduct

L94 ↗
CategoryTheory.PreGaloisCategory.isGalois_of_mono_to_binaryProduct
Documentation

A connected subobject of a product of two Galois objects is Galois. This is the Galois-category form of intersecting two normal open subgroups.

Source context 8 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
open Limits
attribute [local instance] FintypeCat.fintype
Lean source · statement
theorem isGalois_of_mono_to_binaryProduct {X Y Z : C}
    [IsGalois X] [IsGalois Y] [IsConnected Z]
    (i : Z ⟶ X ⨯ Y) [Mono i] :
    IsGalois Z
theorem

autMapHom_prod_injective_of_mono

L136 ↗
CategoryTheory.PreGaloisCategory.autMapHom_prod_injective_of_mono
Documentation

If a connected object is a subobject of a product of two Galois objects, the two induced maps on automorphism groups are jointly injective.

Source context 8 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
open Limits
attribute [local instance] FintypeCat.fintype
Lean source · statement
theorem autMapHom_prod_injective_of_mono {X Y Z : C}
    [IsGalois X] [IsGalois Y] [IsConnected Z]
    (i : Z ⟶ X ⨯ Y) [Mono i] :
    Function.Injective
      (MonoidHom.prod (autMapHom (i ≫ prod.fst)) (autMapHom (i ≫ prod.snd)))
theorem

exists_common_galois_cover

L161 ↗
CategoryTheory.PreGaloisCategory.exists_common_galois_cover
Documentation

Two Galois objects have a common Galois cover. Its automorphism group maps injectively to the product of the two original automorphism groups.

Source context 8 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
open Limits
attribute [local instance] FintypeCat.fintype
Lean source · full declaration
theorem exists_common_galois_cover (X Y : C) [IsGalois X] [IsGalois Y] :
    ∃ (Z : C) (hZ : IsGalois Z),
      letI := hZ
      ∃ (f : Z ⟶ X) (g : Z ⟶ Y),
        Function.Injective (MonoidHom.prod (autMapHom f) (autMapHom g)) := by
  let F := CategoryTheory.GaloisCategory.getFiberFunctor C
  let x : F.obj X := Classical.choice inferInstance
  let y : F.obj Y := Classical.choice inferInstance
  obtain ⟨Z, i, _, _, hZ, hi⟩ := fiber_in_connected_component F (X ⨯ Y)
    ((fiberBinaryProductEquiv F X Y).symm (x, y))
  let : IsConnected Z := hZ
  let : Mono i := hi
  have hGalois : IsGalois Z := isGalois_of_mono_to_binaryProduct i
  let : IsGalois Z := hGalois
  exact ⟨Z, hGalois, i ≫ prod.fst, i ≫ prod.snd,
    autMapHom_prod_injective_of_mono i⟩
theorem

natCard_left_eq_finrank

L191 ↗
AlgebraicGeometry.FiniteEtale.natCard_left_eq_finrank
Documentation

Over a separably closed field, the number of points of a finite étale scheme is the rank of its structure morphism.

Source context 7 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
open CategoryTheory
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
Lean source · statement
theorem natCard_left_eq_finrank (X : FiniteEtale (Spec (.of Ω))) :
    Nat.card X.left = X.hom.finrank (IsLocalRing.closedPoint Ω)
theorem

natCard_fiber_eq_finrank

L206 ↗
AlgebraicGeometry.FiniteEtale.natCard_fiber_eq_finrank
Documentation

The cardinality of the geometric fiber of a finite étale morphism is its rank at the image of the geometric point.

Source context 8 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
open CategoryTheory
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable {S : Scheme.{u}} (ξ : Spec (.of Ω) ⟶ S)
Lean source · statement
theorem natCard_fiber_eq_finrank (X : FiniteEtale S) :
    Nat.card ((fiber ξ).obj X) =
      X.hom.finrank (ξ (IsLocalRing.closedPoint Ω))
theorem

isGalois_iff_card_aut_eq_finrank

L231 ↗
AlgebraicGeometry.FiniteEtale.isGalois_iff_card_aut_eq_finrank
Documentation

Scheme-theoretic degree form of the automorphism-cardinality characterization of a connected finite étale Galois cover.

Source context 9 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
open CategoryTheory
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable {S : Scheme.{u}} (ξ : Spec (.of Ω) ⟶ S)
variable [ConnectedSpace S]
Lean source · statement
theorem isGalois_iff_card_aut_eq_finrank
    (X : FiniteEtale S) [PreGaloisCategory.IsConnected X] :
    PreGaloisCategory.IsGalois X ↔
      Nat.card (Aut X) = X.hom.finrank (ξ (IsLocalRing.closedPoint Ω))
theorem

isGalois_iff_isConnected_and_card_aut_eq_finrank

L241 ↗
AlgebraicGeometry.FiniteEtale.isGalois_iff_isConnected_and_card_aut_eq_finrank
Documentation

A finite étale cover is Galois exactly when it is connected and its automorphism group has cardinality equal to its degree.

Source context 9 commands

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

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
open CategoryTheory
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable {S : Scheme.{u}} (ξ : Spec (.of Ω) ⟶ S)
variable [ConnectedSpace S]
Lean source · statement
theorem isGalois_iff_isConnected_and_card_aut_eq_finrank (X : FiniteEtale S) :
    PreGaloisCategory.IsGalois X ↔
      PreGaloisCategory.IsConnected X ∧
        Nat.card (Aut X) = X.hom.finrank (ξ (IsLocalRing.closedPoint Ω))

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