Module

FiberIsoKernel.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.FiberIsoKernel

2 declarations indexed from sourceView source ↗

Module documentation

Kernels and fixed fibers under a change of fiber functor

A natural isomorphism transports the kernel of restriction to another fiber functor. It also transports fixed points of the induced automorphisms. These are the two compatibility statements needed to use arbitrary geometric paths.

Imports1

Nyll.EtaleFundamentalGroups.GaloisCategories.FiberIso

Imported by2

theorem

autHomOfCompIso_conj_eq_one_of_eq_one

L29 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso_conj_eq_one_of_eq_one

Documentation

Changing the source and target fiber comparisons preserves the kernel of restriction along a functor.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w
variable {C : Type u} [Category.{v} C] {C' : Type u'} [Category.{v'} C']

Lean source · statement

theorem autHomOfCompIso_conj_eq_one_of_eq_one
    (H : C ⥤ C') {F G : C' ⥤ FintypeCat.{w}}
    {F₀ G₀ : C ⥤ FintypeCat.{w}}
    (t : F ≅ G) (s : H ⋙ F ≅ F₀) (r : H ⋙ G ≅ G₀)
    (a : Aut F) (ha : autHomOfCompIso H s a = 1) :
    autHomOfCompIso H r (continuousConjAut t a) = 1

theorem

fiber_fixed_of_conj_fixed

L51 ↗

CategoryTheory.PreGaloisCategory.fiber_fixed_of_conj_fixed