Module

AutFunctorComparison.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.AutFunctorComparison

4 declarations indexed from sourceView source ↗

Module documentation

Coherent maps on automorphism groups

The maps induced by composite functors compose strictly with the composite comparison. Replacing a functor by a naturally isomorphic one, and using that isomorphism in the fiber comparison, leaves the induced map unchanged.

Imports1

Nyll.EtaleFundamentalGroups.GaloisCategories.Functoriality

Imported by2

theorem

autHomOfCompIso_isoFunctor

L31 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso_isoFunctor

Documentation

A natural isomorphism between the source functors does not alter the induced automorphism map when included in the comparison.

Source context 7 commands

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

noncomputable section
universe u₁ u₂ v₁ v₂ w₁ w₂ z
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable {D : Type v₁} [Category.{v₂} D]
variable {E : Type w₁} [Category.{w₂} E]

Lean source · statement

theorem autHomOfCompIso_isoFunctor
    {H K : C ⥤ D} (α : H ≅ K) {F : D ⥤ FintypeCat.{z}}
    {G : C ⥤ FintypeCat.{z}} (t : K ⋙ F ≅ G) (a : Aut F) :
    autHomOfCompIso H (Functor.isoWhiskerRight α F ≪≫ t) a =
      autHomOfCompIso K t a

theorem

autHomOfCompIso_comp

L49 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso_comp

Documentation

Induction on automorphism groups is compatible with composite functors and their explicit composite fiber comparison.

Source context 7 commands

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

noncomputable section
universe u₁ u₂ v₁ v₂ w₁ w₂ z
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable {D : Type v₁} [Category.{v₂} D]
variable {E : Type w₁} [Category.{w₂} E]

Lean source · statement

theorem autHomOfCompIso_comp
    (H : C ⥤ D) (K : D ⥤ E)
    {F : E ⥤ FintypeCat.{z}} {G : D ⥤ FintypeCat.{z}}
    {L : C ⥤ FintypeCat.{z}} (tK : K ⋙ F ≅ G) (tH : H ⋙ G ≅ L)
    (a : Aut F) :
    autHomOfCompIso (H ⋙ K)
        (Functor.associator H K F ≪≫ Functor.isoWhiskerLeft H tK ≪≫ tH) a =
      autHomOfCompIso H tH (autHomOfCompIso K tK a)

def

transportedEndofunctorFiberIso

L63 ↗

CategoryTheory.PreGaloisCategory.transportedEndofunctorFiberIso

Documentation

Transfer a pointed endofunctor through a comparison functor and a specified commuting square of functors.

Source context 7 commands

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

noncomputable section
universe u₁ u₂ v₁ v₂ w₁ w₂ z
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable {D : Type v₁} [Category.{v₂} D]
variable {E : Type w₁} [Category.{w₂} E]

Lean source · statement

def transportedEndofunctorFiberIso
    (H : C ⥤ D) (K : C ⥤ C) (L : D ⥤ D)
    {F : D ⥤ FintypeCat.{z}} {G : C ⥤ FintypeCat.{z}}
    (e : H ⋙ F ≅ G) (κ : K ⋙ H ≅ H ⋙ L) (t : L ⋙ F ≅ F) :
    K ⋙ G ≅ G

theorem

autHomOfCompIso_transportedEndofunctor

L76 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso_transportedEndofunctor

Documentation

The transferred endofunctor induces the same automorphism action under the original comparison of fiber functors.

Source context 7 commands

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

noncomputable section
universe u₁ u₂ v₁ v₂ w₁ w₂ z
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable {D : Type v₁} [Category.{v₂} D]
variable {E : Type w₁} [Category.{w₂} E]

Lean source · statement

theorem autHomOfCompIso_transportedEndofunctor
    (H : C ⥤ D) (K : C ⥤ C) (L : D ⥤ D)
    {F : D ⥤ FintypeCat.{z}} {G : C ⥤ FintypeCat.{z}}
    (e : H ⋙ F ≅ G) (κ : K ⋙ H ≅ H ⋙ L) (t : L ⋙ F ≅ F)
    (a : Aut F) :
    autHomOfCompIso K (transportedEndofunctorFiberIso H K L e κ t)
        (autHomOfCompIso H e a) =
      autHomOfCompIso H e (autHomOfCompIso L t a)

Module documentation

Coherent maps on automorphism groups

Declarations

autHomOfCompIso_isoFunctor

autHomOfCompIso_comp

transportedEndofunctorFiberIso

autHomOfCompIso_transportedEndofunctor