Module

Surjectivity.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.Surjectivity

9 declarations indexed from sourceView source ↗

Module documentation

Surjectivity criteria for functors of Galois categories

The continuous homomorphism on automorphism groups induced by a functor of Galois categories is surjective exactly when the functor is fully faithful. Equivalently, it preserves connected objects, lifts points of connected objects, or induces bijections on points.

Imports8

Nyll.EtaleFundamentalGroups.GaloisCategories.ContinuousHomComparison
Nyll.EtaleFundamentalGroups.GaloisCategories.ConnectedActions
Nyll.EtaleFundamentalGroups.ContinuousActions.RestrictionFullyFaithful
Mathlib.Data.List.TFAE
Mathlib.GroupTheory.GroupAction.Quotient
Mathlib.GroupTheory.GroupAction.Transitive
Mathlib.Topology.Algebra.ClopenNhdofOne
Mathlib.Topology.Algebra.OpenSubgroup

Imported by10

theorem

exists_open_supergroup

L38 ↗

CategoryTheory.PreGaloisCategory.exists_open_supergroup

Source context 6 commands

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

@[expose] public section
universe g g' u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory

Lean source · statement

theorem exists_open_supergroup
    {G' : Type g'} {G : Type g}
    [Group G'] [TopologicalSpace G'] [CompactSpace G']
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G] [T2Space G]
    (h : G' →ₜ* G) (nh : ¬ Function.Surjective h) :
    ∃ U : Subgroup G, IsOpen (U : Set G) ∧
      h.toMonoidHom.range ≤ U ∧ U ≠ ⊤

theorem

exists_small_action

L70 ↗

CategoryTheory.PreGaloisCategory.exists_small_action

Source context 6 commands

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

@[expose] public section
universe g g' u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory

Lean source · statement

theorem exists_small_action
    {G' : Type g'} {G : Type g}
    [Group G'] [TopologicalSpace G']
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (h : G' →ₜ* G) (U : Subgroup G)
    (hUopen : IsOpen (U : Set G))
    (hKU : h.toMonoidHom.range ≤ U) (hUne : U ≠ ⊤) :
    ∃ (Y : ContAction FintypeCat.{w} G) (y : Y.obj.V),
      MulAction.IsPretransitive G Y.obj.V ∧
      (∀ a : G', h a • y = y) ∧ ¬ Subsingleton Y.obj.V

theorem

point_lifting_implies_surjective

L157 ↗

CategoryTheory.PreGaloisCategory.point_lifting_implies_surjective

Source context 11 commands

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

@[expose] public section
universe g g' u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']
variable (H : C ⥤ C')

Lean source · statement

theorem point_lifting_implies_surjective
    (t : H ⋙ F' ≅ F)
    (h4 : ∀ X : C, IsConnected X →
      Nonempty (⊤_ C' ⟶ H.obj X) → Nonempty (⊤_ C ⟶ X)) :
    Function.Surjective (autHomOfCompIso H t)

theorem

surjective_implies_fullyFaithful

L237 ↗

CategoryTheory.PreGaloisCategory.surjective_implies_fullyFaithful

Source context 11 commands

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

@[expose] public section
universe g g' u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']
variable (H : C ⥤ C')

Lean source · statement

theorem surjective_implies_fullyFaithful
    (t : H ⋙ F' ≅ F)
    (hs : Function.Surjective (autHomOfCompIso H t)) :
    Nonempty H.FullyFaithful

theorem

surjective_implies_connected

L253 ↗

CategoryTheory.PreGaloisCategory.surjective_implies_connected

Source context 11 commands

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

@[expose] public section
universe g g' u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']
variable (H : C ⥤ C')

Lean source · statement

theorem surjective_implies_connected
    (t : H ⋙ F' ≅ F)
    (hs : Function.Surjective (autHomOfCompIso H t)) :
    ∀ X : C, IsConnected X → IsConnected (H.obj X)

theorem

fullyFaithful_implies_points

L287 ↗

CategoryTheory.PreGaloisCategory.fullyFaithful_implies_points

Source context 11 commands

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

@[expose] public section
universe g g' u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']
variable (H : C ⥤ C')

Lean source · full declaration

theorem fullyFaithful_implies_points
    [PreservesLimitsOfShape (Discrete PEmpty.{1}) H]
    (hff : Nonempty H.FullyFaithful) :
    ∀ X : C, Function.Bijective
      (fun f : (⊤_ C ⟶ X) ↦
        (PreservesTerminal.iso H).inv ≫ H.map f) := by
  intro X
  let ff := hff.some
  constructor
  · intro f g hfg
    apply ff.map_injective
    simpa using
      (cancel_epi (PreservesTerminal.iso H).inv).mp hfg
  · intro q
    let f := ff.preimage ((PreservesTerminal.iso H).hom ≫ q)
    refine ⟨f, ?_⟩
    dsimp [f]
    rw [ff.map_preimage]
    rw [← PreservesTerminal.iso_hom]
    exact (PreservesTerminal.iso H).inv_hom_id_assoc q

theorem

points_imply_point_lifting

L308 ↗

CategoryTheory.PreGaloisCategory.points_imply_point_lifting

Source context 11 commands

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

@[expose] public section
universe g g' u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']
variable (H : C ⥤ C')

Lean source · full declaration

theorem points_imply_point_lifting
    [PreservesLimitsOfShape (Discrete PEmpty.{1}) H]
    (h5 : ∀ X : C, Function.Bijective
      (fun f : (⊤_ C ⟶ X) ↦
        (PreservesTerminal.iso H).inv ≫ H.map f)) :
    ∀ X : C, IsConnected X →
      Nonempty (⊤_ C' ⟶ H.obj X) → Nonempty (⊤_ C ⟶ X) := by
  intro X _ hq
  obtain ⟨f, _⟩ := (h5 X).surjective hq.some
  exact ⟨f⟩

theorem

connected_implies_point_lifting

L319 ↗

CategoryTheory.PreGaloisCategory.connected_implies_point_lifting

Source context 11 commands

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

@[expose] public section
universe g g' u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']
variable (H : C ⥤ C')

Lean source · statement

theorem connected_implies_point_lifting
    (t : H ⋙ F' ≅ F)
    (h3 : ∀ X : C, IsConnected X → IsConnected (H.obj X)) :
    ∀ X : C, IsConnected X →
      Nonempty (⊤_ C' ⟶ H.obj X) → Nonempty (⊤_ C ⟶ X)

theorem

autHomOfCompIso_surjective_tfae

L351 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso_surjective_tfae

Documentation

The five equivalent surjectivity criteria for the homomorphism on fundamental groups induced by a functor of Galois categories.

Source context 11 commands

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

@[expose] public section
universe g g' u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']
variable (H : C ⥤ C')

Lean source · full declaration

theorem autHomOfCompIso_surjective_tfae
    [PreservesLimitsOfShape (Discrete PEmpty.{1}) H]
    (t : H ⋙ F' ≅ F) :
    List.TFAE [
      Function.Surjective (autHomOfCompIso H t),
      Nonempty H.FullyFaithful,
      ∀ X : C, IsConnected X → IsConnected (H.obj X),
      ∀ X : C, IsConnected X →
        Nonempty (⊤_ C' ⟶ H.obj X) → Nonempty (⊤_ C ⟶ X),
      ∀ X : C, Function.Bijective
        (fun f : (⊤_ C ⟶ X) ↦
          (PreservesTerminal.iso H).inv ≫ H.map f)] := by
  tfae_have 1 → 2 :=
    surjective_implies_fullyFaithful F F' H t
  tfae_have 1 → 3 :=
    surjective_implies_connected F F' H t
  tfae_have 2 → 5 :=
    fullyFaithful_implies_points H
  tfae_have 5 → 4 :=
    points_imply_point_lifting H
  tfae_have 3 → 4 :=
    connected_implies_point_lifting F F' H t
  tfae_have 4 → 1 :=
    point_lifting_implies_surjective F F' H t
  tfae_finish

Module documentation

Surjectivity criteria for functors of Galois categories

Declarations