Module

AutomorphismInverseLimit.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.AutomorphismInverseLimit

18 declarations indexed from sourceView source ↗

Module documentation

Automorphism groups of a category assembled from stages

The transition homomorphisms are restriction followed by the specified cone isomorphism. Identity and composition follow from ordinary functor coherence. Joint essential surjectivity and eventual morphism descent make the resulting continuous comparison bijective. Compactness then upgrades it to an isomorphism of topological groups. No individual restriction or inverse-limit projection is assumed surjective.

Imports4

Imported by2

def

stageAutRestriction

L42 ↗

CategoryTheory.PreGaloisCategory.stageAutRestriction

Documentation

Restriction to the later stage, transported back by the cone comparison.

Source context 13 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})

Lean source · statement

def stageAutRestriction {i j : I} (hij : i ≤ j) :
    Aut (H j ⋙ F) →ₜ* Aut (H i ⋙ F)

theorem

stageAutRestriction_hom_app

L48 ↗

CategoryTheory.PreGaloisCategory.stageAutRestriction_hom_app

Documentation

The component formula for the constructed transition homomorphism.

Source context 13 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})

Lean source · statement

theorem stageAutRestriction_hom_app {i j : I} (hij : i ≤ j)
    (a : Aut (H j ⋙ F)) (A : Cstage i) :
    (stageAutRestriction Cstage H T e F hij a).hom.app A =
      F.map ((e hij).hom.app A) ≫ a.hom.app ((T hij).obj A) ≫
        F.map ((e hij).inv.app A)

theorem

stageAutRestriction_commutes

L63 ↗

CategoryTheory.PreGaloisCategory.stageAutRestriction_commutes

Documentation

The restriction formula expressed as its conjugation square.

Source context 13 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})

Lean source · statement

theorem stageAutRestriction_commutes {i j : I} (hij : i ≤ j)
    (a : Aut (H j ⋙ F)) (A : Cstage i) :
    F.map ((e hij).hom.app A) ≫ a.hom.app ((T hij).obj A) =
      (stageAutRestriction Cstage H T e F hij a).hom.app A ≫
        F.map ((e hij).hom.app A)

theorem

cone_identity_component

L88 ↗

CategoryTheory.PreGaloisCategory.cone_identity_component

Source context 18 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
include he_id in

Lean source · statement

theorem cone_identity_component (i : I) (A : Cstage i) :
    (e (le_rfl : i ≤ i)).hom.app A = (H i).map ((d i).inv.app A)

theorem

cone_composition_component

L101 ↗

CategoryTheory.PreGaloisCategory.cone_composition_component

Source context 18 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
include he_comp in

Lean source · statement

theorem cone_composition_component {i j k : I}
    (hij : i ≤ j) (hjk : j ≤ k) (A : Cstage i) :
    F.map ((e (hij.trans hjk)).hom.app A) ≫
        F.map ((H k).map ((c hij hjk).hom.app A)) =
      F.map ((e hij).hom.app A) ≫
        F.map ((e hjk).hom.app ((T hij).obj A))

theorem

stageAutRestriction_id

L119 ↗

CategoryTheory.PreGaloisCategory.stageAutRestriction_id

Documentation

Identity refinement induces the identity on the automorphism group.

Source context 18 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
include he_id in

Lean source · statement

theorem stageAutRestriction_id (i : I) (a : Aut (H i ⋙ F)) :
    stageAutRestriction Cstage H T e F (le_rfl : i ≤ i) a = a

theorem

stageAutRestriction_comp

L131 ↗

CategoryTheory.PreGaloisCategory.stageAutRestriction_comp

Documentation

Composed refinement induces the composite of the constructed restrictions.

Source context 18 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
include he_comp in

Lean source · statement

theorem stageAutRestriction_comp {i j k : I}
    (hij : i ≤ j) (hjk : j ≤ k) (a : Aut (H k ⋙ F)) :
    stageAutRestriction Cstage H T e F hij
        (stageAutRestriction Cstage H T e F hjk a) =
      stageAutRestriction Cstage H T e F (hij.trans hjk) a

def

autInverseSystem

L169 ↗

CategoryTheory.PreGaloisCategory.autInverseSystem

Documentation

The inverse system of actual stage automorphism groups. Reducibility keeps the stage group instances definitionally those of the supplied functors.

Source context 17 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))

Lean source · full declaration

def autInverseSystem : InverseSystem (I := I) where
  X i := Aut (H i ⋙ F)
  topologicalSpace i := inferInstance
  map hij := stageAutRestriction Cstage H T e F hij
  continuous_map hij := (stageAutRestriction Cstage H T e F hij).continuous_toFun
  map_id i := by
    funext a
    exact stageAutRestriction_id Cstage H T e F d he_id i a
  map_comp hij hjk := by
    funext a
    exact stageAutRestriction_comp Cstage H T e F c he_comp hij hjk a

instance

autInverseSystem_isGroupSystem

L182 ↗

CategoryTheory.PreGaloisCategory.autInverseSystem_isGroupSystem

Documentation

The constructed system is group-valued because its maps are homomorphisms.

Source context 17 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))

Lean source · full declaration

instance autInverseSystem_isGroupSystem :
    IsGroupSystem (autInverseSystem Cstage H T e F d c he_id he_comp) where
  map_one hij := (stageAutRestriction Cstage H T e F hij).map_one
  map_mul hij a b := (stageAutRestriction Cstage H T e F hij).map_mul a b
  map_inv hij a := (stageAutRestriction Cstage H T e F hij).map_inv a

def

globalAutRestriction

L190 ↗

CategoryTheory.PreGaloisCategory.globalAutRestriction

Documentation

Restriction of a global automorphism to one stage of the cone.

Source context 18 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
omit [Preorder I] in

Lean source · full declaration

def globalAutRestriction (i : I) : Aut F →ₜ* Aut (H i ⋙ F) where
  toMonoidHom := ((Functor.whiskeringLeft (Cstage i) C FintypeCat.{w}).obj (H i)).mapAut F
  continuous_toFun := continuous_mapAut_whiskeringLeft (H i) F

theorem

globalAutRestriction_compatible

L195 ↗

CategoryTheory.PreGaloisCategory.globalAutRestriction_compatible

Documentation

Global restrictions satisfy the compatibility required by the inverse limit.

Source context 17 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))

Lean source · statement

theorem globalAutRestriction_compatible {i j : I} (hij : i ≤ j) (a : Aut F) :
    stageAutRestriction Cstage H T e F hij (globalAutRestriction Cstage H F j a) =
      globalAutRestriction Cstage H F i a

def

autInverseLimitComparison

L206 ↗

CategoryTheory.PreGaloisCategory.autInverseLimitComparison

Documentation

The canonical comparison sends a global automorphism to all its restrictions.

Source context 17 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))

Lean source · full declaration

def autInverseLimitComparison :
    Aut F →ₜ* (autInverseSystem Cstage H T e F d c he_id he_comp).inverseLimit where
  toFun a := ⟨fun i ↦ globalAutRestriction Cstage H F i a, fun i j hij ↦
    globalAutRestriction_compatible Cstage H T e F hij a⟩
  map_one' := by
    apply Subtype.ext
    funext i
    exact (globalAutRestriction Cstage H F i).map_one
  map_mul' a b := by
    apply Subtype.ext
    funext i
    exact (globalAutRestriction Cstage H F i).map_mul a b
  continuous_toFun := Continuous.subtype_mk
    (continuous_pi fun i ↦ (globalAutRestriction Cstage H F i).continuous_toFun)
    (fun a i j hij ↦ globalAutRestriction_compatible Cstage H T e F hij a)

theorem

autInverseLimitComparison_projection

L223 ↗

CategoryTheory.PreGaloisCategory.autInverseLimitComparison_projection

Documentation

The constructed comparison has the canonical stage coordinate formula.

Source context 17 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))

Lean source · statement

theorem autInverseLimitComparison_projection (i : I) (a : Aut F) :
    (autInverseSystem Cstage H T e F d c he_id he_comp).projection i
        (autInverseLimitComparison Cstage H T e F d c he_id he_comp a) =
      globalAutRestriction Cstage H F i a

theorem

autInverseLimitComparison_injective

L237 ↗

CategoryTheory.PreGaloisCategory.autInverseLimitComparison_injective

Documentation

Joint essential surjectivity detects equality of global automorphisms.

Source context 20 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
variable (hobj : ∀ X : C, ∃ (i : I) (A : Cstage i), Nonempty ((H i).obj A ≅ X))
variable (hhom : ∀ (i j : I) (A : Cstage i) (B : Cstage j)
  (f : (H i).obj A ⟶ (H j).obj B),
  ∃ (k : I) (hik : i ≤ k) (hjk : j ≤ k)
    (g : (T hik).obj A ⟶ (T hjk).obj B),
    f = (e hik).hom.app A ≫ (H k).map g ≫ (e hjk).inv.app B)
include hobj in

Lean source · statement

theorem autInverseLimitComparison_injective :
    Function.Injective (autInverseLimitComparison Cstage H T e F d c he_id he_comp)

theorem

autInverseLimitComparison_surjective

L251 ↗

CategoryTheory.PreGaloisCategory.autInverseLimitComparison_surjective

Documentation

Eventual morphism descent glues each compatible stage family.

Source context 20 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
variable (hobj : ∀ X : C, ∃ (i : I) (A : Cstage i), Nonempty ((H i).obj A ≅ X))
variable (hhom : ∀ (i j : I) (A : Cstage i) (B : Cstage j)
  (f : (H i).obj A ⟶ (H j).obj B),
  ∃ (k : I) (hik : i ≤ k) (hjk : j ≤ k)
    (g : (T hik).obj A ⟶ (T hjk).obj B),
    f = (e hik).hom.app A ≫ (H k).map g ≫ (e hjk).inv.app B)
include hobj hhom in

Lean source · statement

theorem autInverseLimitComparison_surjective :
    Function.Surjective (autInverseLimitComparison Cstage H T e F d c he_id he_comp)

theorem

autInverseLimitComparison_bijective

L273 ↗

CategoryTheory.PreGaloisCategory.autInverseLimitComparison_bijective

Documentation

The canonical comparison is bijective under categorical object and morphism descent.

Source context 20 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
variable (hobj : ∀ X : C, ∃ (i : I) (A : Cstage i), Nonempty ((H i).obj A ≅ X))
variable (hhom : ∀ (i j : I) (A : Cstage i) (B : Cstage j)
  (f : (H i).obj A ⟶ (H j).obj B),
  ∃ (k : I) (hik : i ≤ k) (hjk : j ≤ k)
    (g : (T hik).obj A ⟶ (T hjk).obj B),
    f = (e hik).hom.app A ≫ (H k).map g ≫ (e hjk).inv.app B)
include hobj hhom in

Lean source · statement

theorem autInverseLimitComparison_bijective :
    Function.Bijective (autInverseLimitComparison Cstage H T e F d c he_id he_comp)

def

autInverseLimitEquiv

L280 ↗

CategoryTheory.PreGaloisCategory.autInverseLimitEquiv

Documentation

Automorphisms of the assembled finite-valued functor form the inverse limit of its stage automorphism groups, with their canonical topologies.

Source context 19 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
variable (hobj : ∀ X : C, ∃ (i : I) (A : Cstage i), Nonempty ((H i).obj A ≅ X))
variable (hhom : ∀ (i j : I) (A : Cstage i) (B : Cstage j)
  (f : (H i).obj A ⟶ (H j).obj B),
  ∃ (k : I) (hik : i ≤ k) (hjk : j ≤ k)
    (g : (T hik).obj A ⟶ (T hjk).obj B),
    f = (e hik).hom.app A ≫ (H k).map g ≫ (e hjk).inv.app B)

Lean source · statement

def autInverseLimitEquiv :
    Aut F ≃ₜ* (autInverseSystem Cstage H T e F d c he_id he_comp).inverseLimit

theorem

autInverseLimitEquiv_projection

L288 ↗

CategoryTheory.PreGaloisCategory.autInverseLimitEquiv_projection

Documentation

The topological group equivalence retains the original restriction formula.

Source context 19 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.Functor
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
variable (d : ∀ i, T (le_rfl : i ≤ i) ≅ 𝟭 (Cstage i))
variable (c : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  T (hij.trans hjk) ≅ T hij ⋙ T hjk)
variable (he_id : ∀ i,
  e (le_rfl : i ≤ i) ≪≫ isoWhiskerRight (d i) (H i) ≪≫
    Functor.leftUnitor (H i) = Iso.refl (H i))
variable (he_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
  e (hij.trans hjk) ≪≫ isoWhiskerRight (c hij hjk) (H k) ≪≫
      Functor.associator (T hij) (T hjk) (H k) =
    e hij ≪≫ isoWhiskerLeft (T hij) (e hjk))
variable (hobj : ∀ X : C, ∃ (i : I) (A : Cstage i), Nonempty ((H i).obj A ≅ X))
variable (hhom : ∀ (i j : I) (A : Cstage i) (B : Cstage j)
  (f : (H i).obj A ⟶ (H j).obj B),
  ∃ (k : I) (hik : i ≤ k) (hjk : j ≤ k)
    (g : (T hik).obj A ⟶ (T hjk).obj B),
    f = (e hik).hom.app A ≫ (H k).map g ≫ (e hjk).inv.app B)

Lean source · statement

theorem autInverseLimitEquiv_projection (i : I) (a : Aut F) :
    (autInverseSystem Cstage H T e F d c he_id he_comp).projection i
        (autInverseLimitEquiv Cstage H T e F d c he_id he_comp hobj hhom a) =
      globalAutRestriction Cstage H F i a

Module documentation

Automorphism groups of a category assembled from stages

Declarations