Module

Injectivity.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.Injectivity

4 declarations indexed from sourceView source ↗

Module documentation

Injectivity of the map attached to a functor of Galois categories

The map on profinite automorphism groups induced by a functor of Galois categories is injective exactly when every connected target object admits the epi--mono span of Stacks Project, Tag 0BN7.

Imports3

Imported by2

theorem

categorical_span_of_action_span

L34 ↗

CategoryTheory.PreGaloisCategory.categorical_span_of_action_span

Source context 9 commands

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

noncomputable section
universe u₁ u₂ v₁ v₂ w
open CategoryTheory
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']

Lean source · statement

theorem categorical_span_of_action_span
    (H : C ⥤ C') (t : H ⋙ F' ≅ F)
    (hspan : ∀ X' : ContAction FintypeCat.{w} (Aut F'),
      Nonempty X'.obj.V →
      MulAction.IsPretransitive (Aut F') X'.obj.V →
      ∃ (X : ContAction FintypeCat.{w} (Aut F))
        (Y' : ContAction FintypeCat.{w} (Aut F'))
        (e : Y' ⟶ X')
        (m : Y' ⟶
          (ContAction.res FintypeCat (autHomOfCompIso H t)).obj X),
        Epi e ∧ Mono m) :
    ∀ X' : C', IsConnected X' →
      ∃ (Y' : C') (X : C) (e : Y' ⟶ X') (m : Y' ⟶ H.obj X),
        Epi e ∧ Mono m

theorem

action_span_of_categorical_span

L86 ↗

CategoryTheory.PreGaloisCategory.action_span_of_categorical_span

Source context 9 commands

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

noncomputable section
universe u₁ u₂ v₁ v₂ w
open CategoryTheory
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']

Lean source · statement

theorem action_span_of_categorical_span
    (H : C ⥤ C') (t : H ⋙ F' ≅ F)
    (hspan : ∀ X' : C', IsConnected X' →
      ∃ (Y' : C') (X : C) (e : Y' ⟶ X') (m : Y' ⟶ H.obj X),
        Epi e ∧ Mono m) :
    ∀ Z : ContAction FintypeCat.{w} (Aut F'),
      Nonempty Z.obj.V →
      MulAction.IsPretransitive (Aut F') Z.obj.V →
      ∃ (X : ContAction FintypeCat.{w} (Aut F))
        (Y : ContAction FintypeCat.{w} (Aut F'))
        (q : Y ⟶ Z)
        (i : Y ⟶
          (ContAction.res FintypeCat (autHomOfCompIso H t)).obj X),
        Epi q ∧ Mono i

theorem

autHomOfCompIso_injective_iff_exists_epi_mono_span

L145 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso_injective_iff_exists_epi_mono_span

Documentation

The homomorphism on profinite automorphism groups induced by H and t is injective exactly when every connected object of the target admits an epimorphism from an object that embeds into an object in the image of H.

Source context 9 commands

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

noncomputable section
universe u₁ u₂ v₁ v₂ w
open CategoryTheory
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']

Lean source · statement

theorem autHomOfCompIso_injective_iff_exists_epi_mono_span
    (H : C ⥤ C') (t : H ⋙ F' ≅ F) :
    Function.Injective (autHomOfCompIso H t) ↔
      ∀ X' : C', IsConnected X' →
        ∃ (Y' : C') (X : C)
          (q : Y' ⟶ X') (i : Y' ⟶ H.obj X),
          Epi q ∧ Mono i

theorem

autHomOfCompIso_injective_of_essSurj

L165 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso_injective_of_essSurj

Documentation

Restriction of automorphisms along an essentially surjective functor is injective. No fullness assumption is needed: every target object is already isomorphic to an object in the image.

Source context 9 commands

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

noncomputable section
universe u₁ u₂ v₁ v₂ w
open CategoryTheory
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']

Lean source · statement

theorem autHomOfCompIso_injective_of_essSurj
    (H : Functor C C') [H.EssSurj] (t : H ⋙ F' ≅ F) :
    Function.Injective (autHomOfCompIso H t)

Module documentation

Injectivity of the map attached to a functor of Galois categories

Declarations

categorical_span_of_action_span

action_span_of_categorical_span

autHomOfCompIso_injective_iff_exists_epi_mono_span

autHomOfCompIso_injective_of_essSurj