Transporting the Galois-category axioms along an equivalence

Being a Galois category is a property of a category, not of a presentation of it, so it should transfer along an equivalence. Mathlib states the axioms (SGA1's (G1)–(G3), and (G4)–(G6) for a fibre functor) in terms of limits, colimits and monomorphisms, all of which are preserved and reflected by an equivalence, but it does not record the transfer. This file does.

The point of the transfer is that a category one wants to recognise as Galois is usually not presented as one. The finite covering spaces of a nice base, for instance, are only known to satisfy the axioms because they are equivalent to the finite π₁-sets, which Mathlib proves are a GaloisCategory in Mathlib/CategoryTheory/Galois/Examples.lean; transporting is much cheaper than building finite coproducts, pullbacks and quotients by finite groups of covering spaces by hand.

Only axiom (G3) needs an argument. Given a monomorphism i : A ⟶ B in C, its image under the equivalence is a monomorphism, so it is the inclusion of a direct summand u : Z ⟶ e.functor.obj B in D. The complementary summand is transported back as e.inverse.obj Z, with structure map the preimage under e.functor of e.counit.app Z ≫ u; taking the preimage rather than e.inverse.map u composed with the unit is what makes the colimit check a single rewrite, since e.functor then maps the transported cofan to the original one reindexed by an isomorphism.

Main declarations

• TauCeti.preGaloisCategory_of_equivalence: (G1)–(G3) transfer along an equivalence.
• TauCeti.fiberFunctor_comp_of_equivalence: (G4)–(G6) transfer, so that a fibre functor on D composes with an equivalence C ≌ D to a fibre functor on C.
• TauCeti.galoisCategory_of_equivalence: a category equivalent to a Galois category is a Galois category.
• CategoryTheory.Functor.isFundamentalGroup_comp: a fundamental group of a fibre functor remains one after the functor is transported along an equivalence.

References

• [lenstraGSchemes]: H. W. Lenstra, Galois theory for schemes, Definition 3.1.

theorem TauCeti.preGaloisCategory_of_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) [CategoryTheory.PreGaloisCategory D] : CategoryTheory.PreGaloisCategory C

A category equivalent to a pre-Galois category is a pre-Galois category.

The finite limits and colimits required by (G1) and (G2) transport along the equivalence, and a monomorphism is a direct summand in C exactly when its image is one in D, which is (G3).

theorem TauCeti.fiberFunctor_comp_of_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory D] (F : CategoryTheory.Functor D FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.PreGaloisCategory.FiberFunctor (e.functor.comp F)

A fibre functor stays a fibre functor after composing with an equivalence.

An equivalence preserves all limits and colimits and reflects isomorphisms, so each of (G4)–(G6) for F gives the same axiom for e.functor ⋙ F.

theorem TauCeti.galoisCategory_of_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (e : C ≌ D) [CategoryTheory.GaloisCategory D] : CategoryTheory.GaloisCategory C

A category equivalent to a Galois category is a Galois category.

Unlike preGaloisCategory_of_equivalence and fiberFunctor_comp_of_equivalence, this fixes the morphism universe of D to that of C. Mathlib's GaloisCategory D asks for a fibre functor into FintypeCat.{v₂}, while GaloisCategory C asks for one into FintypeCat.{v₁}, and there is no universe-lowering functor between the two to bridge the gap.

@[instance_reducible]

def CategoryTheory.Functor.mulActionComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (K : Functor C D) (F : Functor D FintypeCat) (G : Type u_1) [Group G] [(Y : D) → MulAction G (F.obj Y).obj] (X : C) : MulAction G ((K.comp F).obj X).obj

The action on a fibre functor, pulled back along a functor on its source category.

Equations

• K.mulActionComp F G X = id inferInstance

theorem CategoryTheory.Functor.isNaturalSMul_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (K : Functor C D) (F : Functor D FintypeCat) (G : Type u_1) [Group G] [(Y : D) → MulAction G (F.obj Y).obj] [PreGaloisCategory.IsNaturalSMul F G] : PreGaloisCategory.IsNaturalSMul (K.comp F) G

A natural action on a fibre functor remains natural after precomposition.

theorem CategoryTheory.Functor.isFundamentalGroup_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (K : Functor C D) (F : Functor D FintypeCat) (G : Type u_1) [Group G] [(Y : D) → MulAction G (F.obj Y).obj] [K.IsEquivalence] [GaloisCategory C] [GaloisCategory D] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [PreGaloisCategory.IsFundamentalGroup F G] : PreGaloisCategory.IsFundamentalGroup (K.comp F) G

A fundamental group of a fibre functor remains a fundamental group after transport along an equivalence of its source category.

The action on each transported fibre is the original action on the corresponding object.