Pro-Representability of fiber functors

We show that any fiber functor is pro-representable, i.e. there exists a pro-object X : I ⥤ C such that F is naturally isomorphic to the colimit of X ⋙ coyoneda.

From this we deduce the canonical isomorphism of Aut F with the limit over the automorphism groups of all Galois objects.

Main definitions

• PointedGaloisObject: the category of pointed Galois objects
• PointedGaloisObject.cocone: a cocone on (PointedGaloisObject.incl F).op ≫ coyoneda with point F ⋙ FintypeCat.incl.
• autGaloisSystem: the system of automorphism groups indexed by the pointed Galois objects.

Main results

• PointedGaloisObject.isColimit: the cocone PointedGaloisObject.cocone is a colimit cocone.
• autMulEquivAutGalois: Aut F is canonically isomorphic to the limit over the automorphism groups of all Galois objects.
• FiberFunctor.isPretransitive_of_isConnected: The Aut F action on the fiber of a connected object is transitive.

Implementation details

The pro-representability statement and the isomorphism of Aut F with the limit over the automorphism groups of all Galois objects naturally forces F to take values in FintypeCat.{u₂} where u₂ is the Hom-universe of C. Since this is used to show that Aut F acts transitively on F.obj X for connected X, we a priori only obtain this result for the mentioned specialized universe setup. To obtain the result for F taking values in an arbitrary FintypeCat.{w}, we postcompose with an equivalence FintypeCat.{w} ≌ FintypeCat.{u₂} and apply the specialized result.

In the following the section Specialized is reserved for the setup where F takes values in FintypeCat.{u₂} and the section General contains results holding for F taking values in an arbitrary FintypeCat.{w}.

References

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

structure CategoryTheory.PreGaloisCategory.PointedGaloisObject {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) : Type (max u₁ u₂ w)

A pointed Galois object is a Galois object with a fixed point of its fiber.

• obj : C

  The underlying object of C.

• pt : ↑(F.obj self.obj)

  An element of the fiber of obj.

• isGalois : CategoryTheory.PreGaloisCategory.IsGalois self.obj

  obj is Galois.

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.isGalois {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {F : CategoryTheory.Functor C FintypeCat} (self : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : CategoryTheory.PreGaloisCategory.IsGalois self.obj

obj is Galois.

instance CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCoeDep {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) (X : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : CoeDep (CategoryTheory.PreGaloisCategory.PointedGaloisObject F) X C

Equations

• CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCoeDep F X = { coe := X.obj }

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.GaloisCategory C} {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {x y : A.Hom B}, x.val = y.val → x = y

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.ext_iff {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.GaloisCategory C} {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {x y : A.Hom B}, x = y ↔ x.val = y.val

structure CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {F : CategoryTheory.Functor C FintypeCat} (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) (B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : Type u₂

The type of homomorphisms between two pointed Galois objects. This is a homomorphism of the underlying objects of C that maps the distinguished points to each other.

• val : A.obj ⟶ B.obj

  The underlying homomorphism of C.

• comp : F.map self.val A.pt = B.pt

  The distinguished point of A is mapped to the distinguished point of B.

@[simp]

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {F : CategoryTheory.Functor C FintypeCat} {A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (self : A.Hom B) : F.map self.val A.pt = B.pt

The distinguished point of A is mapped to the distinguished point of B.

instance CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCategory {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) : CategoryTheory.Category.{u₂, max (max w u₂) u₁} (CategoryTheory.PreGaloisCategory.PointedGaloisObject F)

The category of pointed Galois objects.

Equations

• CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCategory F = CategoryTheory.Category.mk ⋯ ⋯ ⋯

instance CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCoeHomHomObj {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) {A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} : Coe (A.Hom B) (A.obj ⟶ B.obj)

Equations

• CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCoeHomHomObj F = { coe := fun (f : A.Hom B) => f.val }

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {F : CategoryTheory.Functor C FintypeCat} {A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {f : A ⟶ B} {g : A ⟶ B} : f = g ↔ f.val = g.val

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.hom_ext {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {F : CategoryTheory.Functor C FintypeCat} {A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {f : A ⟶ B} {g : A ⟶ B} (h : f.val = g.val) : f = g

@[simp]

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.id_val {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {F : CategoryTheory.Functor C FintypeCat} (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : (CategoryTheory.CategoryStruct.id A).val = CategoryTheory.CategoryStruct.id A.obj

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.comp_val_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C✝] [CategoryTheory.GaloisCategory C✝] {F : CategoryTheory.Functor C✝ FintypeCat} {A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {C : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : A ⟶ B) (g : B ⟶ C) {Z : C✝} (h : C.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val h = CategoryTheory.CategoryStruct.comp f.val (CategoryTheory.CategoryStruct.comp g.val h)

@[simp]

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.comp_val {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C✝] [CategoryTheory.GaloisCategory C✝] {F : CategoryTheory.Functor C✝ FintypeCat} {A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {C : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : A ⟶ B) (g : B ⟶ C) : (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val

def CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) : CategoryTheory.Functor (CategoryTheory.PreGaloisCategory.PointedGaloisObject F) C

The canonical functor from pointed Galois objects to C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl_obj {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : (CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).obj A = A.obj

@[simp]

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl_map {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) {A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : A ⟶ B) : (CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).map f = f.val

def CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) : CategoryTheory.Limits.Cocone ((CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).op.comp CategoryTheory.coyoneda)

F ⋙ FintypeCat.incl as a cocone over (can F).op ⋙ coyoneda. This is a colimit cocone (see PreGaloisCategory.isColimìt)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) (B : C) (f : A.obj ⟶ B) : ((CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone F).ι.app (Opposite.op A)).app B f = F.map f A.pt

instance CategoryTheory.PreGaloisCategory.PointedGaloisObject.instIsCofilteredOrEmpty {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.IsCofilteredOrEmpty (CategoryTheory.PreGaloisCategory.PointedGaloisObject F)

The category of pointed Galois objects is cofiltered.

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.PreGaloisCategory.PointedGaloisObject.isColimit {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Limits.IsColimit (CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone F)

cocone F is a colimit cocone, i.e. F is pro-represented by incl F.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.PreGaloisCategory.PointedGaloisObject.instHasColimitOppositeFunctorTypeCompOpInclCoyoneda {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Limits.HasColimit ((CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).op.comp CategoryTheory.coyoneda)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.PreGaloisCategory.autGaloisSystem_obj {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : (CategoryTheory.PreGaloisCategory.autGaloisSystem F).obj A = Grp.of (CategoryTheory.Aut A.obj)

@[simp]

theorem CategoryTheory.PreGaloisCategory.autGaloisSystem_map {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) {A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} {B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : A ⟶ B) : (CategoryTheory.PreGaloisCategory.autGaloisSystem F).map f = CategoryTheory.PreGaloisCategory.autMapHom f.val

noncomputable def CategoryTheory.PreGaloisCategory.autGaloisSystem {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) : CategoryTheory.Functor (CategoryTheory.PreGaloisCategory.PointedGaloisObject F) Grp

The diagram sending each pointed Galois object to its automorphism group as an object of C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.PreGaloisCategory.AutGalois {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) : Type (max u₁ u₂)

The limit of autGaloisSystem.

Equations

• CategoryTheory.PreGaloisCategory.AutGalois F = ↑((CategoryTheory.PreGaloisCategory.autGaloisSystem F).comp (CategoryTheory.forget Grp)).sections

noncomputable instance CategoryTheory.PreGaloisCategory.instGroupAutGalois {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) : Group (CategoryTheory.PreGaloisCategory.AutGalois F)

Equations

• CategoryTheory.PreGaloisCategory.instGroupAutGalois F = inferInstanceAs (Group ↑((CategoryTheory.PreGaloisCategory.autGaloisSystem F).comp (CategoryTheory.forget Grp)).sections)

noncomputable def CategoryTheory.PreGaloisCategory.AutGalois.π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : CategoryTheory.PreGaloisCategory.AutGalois F →* CategoryTheory.Aut A.obj

The canonical projection from AutGalois F to the C-automorphism group of each pointed Galois object.

Equations

• CategoryTheory.PreGaloisCategory.AutGalois.π F A = Grp.sectionsπMonoidHom (CategoryTheory.PreGaloisCategory.autGaloisSystem F) A

theorem CategoryTheory.PreGaloisCategory.AutGalois.π_apply {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) (x : CategoryTheory.PreGaloisCategory.AutGalois F) : (CategoryTheory.PreGaloisCategory.AutGalois.π F A) x = ↑x A

theorem CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) ⦃A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F⦄ ⦃B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F⦄ (f : A ⟶ B) : Function.Surjective ⇑((CategoryTheory.PreGaloisCategory.autGaloisSystem F).map f)

theorem CategoryTheory.PreGaloisCategory.AutGalois.ext {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) {f : CategoryTheory.PreGaloisCategory.AutGalois F} {g : CategoryTheory.PreGaloisCategory.AutGalois F} (h : ∀ (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F), (CategoryTheory.PreGaloisCategory.AutGalois.π F A) f = (CategoryTheory.PreGaloisCategory.AutGalois.π F A) g) : f = g

Equality of elements of AutGalois F can be checked on the projections on each pointed Galois object.

theorem CategoryTheory.PreGaloisCategory.AutGalois.π_surjective {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.AutGalois.π F A)

autGalois.π is surjective for every pointed Galois object.

Isomorphism between Aut F and AutGalois F

In this section we establish the isomorphism between the automorphism group of F and the limit over the automorphism groups of all Galois objects.

We first establish the isomorphism between End F and AutGalois F, from which we deduce that End F is a group, hence End F = Aut F. The isomorphism is built in multiple steps:

• endEquivSectionsFibers : End F ≅ (incl F ⋙ F').sections: the endomorphisms of F are isomorphic to the limit over F.obj A for all Galois objects A. This is obtained as the composition (slightly simplified):

  End F ≅ (colimit ((incl F).op ⋙ coyoneda) ⟶ F) ≅ (incl F ⋙ F).sections

  Where the first isomorphism is induced from the pro-representability of F and the second one from the pro-coyoneda lemma.

• endEquivAutGalois : End F ≅ AutGalois F: this is the composition of endEquivSectionsFibers with:

  (incl F ⋙ F).sections ≅ (autGaloisSystem F ⋙ forget Grp).sections

  which is induced from the level-wise equivalence Aut A ≃ F.obj A for a Galois object A.

noncomputable def CategoryTheory.PreGaloisCategory.endEquivSectionsFibers {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.End F ≃ ↑((CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).comp (F.comp FintypeCat.incl)).sections

The endomorphisms of F are isomorphic to the limit over the fibers of F on all Galois objects.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : ↑((CategoryTheory.PreGaloisCategory.endEquivSectionsFibers F) f) A = f.app A.obj A.pt

noncomputable def CategoryTheory.PreGaloisCategory.autIsoFibers {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.autGaloisSystem F).comp (CategoryTheory.forget Grp) ≅ (CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).comp (F.comp FintypeCat.incl)

Functorial isomorphism Aut A ≅ F.obj A for Galois objects A.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) (b : ↑(F.obj A.obj)) : (CategoryTheory.PreGaloisCategory.autIsoFibers F).inv.app A b = (CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A.obj A.pt).symm b

noncomputable def CategoryTheory.PreGaloisCategory.endEquivAutGalois {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.End F ≃ CategoryTheory.PreGaloisCategory.AutGalois F

The equivalence between endomorphisms of F and the limit over the automorphism groups of all Galois objects.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.PreGaloisCategory.endEquivAutGalois_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F A) ((CategoryTheory.PreGaloisCategory.endEquivAutGalois F) f)).hom A.pt = f.app A.obj A.pt

@[simp]

theorem CategoryTheory.PreGaloisCategory.endEquivAutGalois_mul {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) (g : CategoryTheory.End F) : (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) (CategoryTheory.CategoryStruct.comp g f) = (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) g * (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) f

noncomputable def CategoryTheory.PreGaloisCategory.endMulEquivAutGalois {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.End F ≃* (CategoryTheory.PreGaloisCategory.AutGalois F)ᵐᵒᵖ

The monoid isomorphism between endomorphisms of F and the (multiplicative opposite of the) limit of automorphism groups of all Galois objects.

Equations

• CategoryTheory.PreGaloisCategory.endMulEquivAutGalois F = { toEquiv := (CategoryTheory.PreGaloisCategory.endEquivAutGalois F).trans MulOpposite.opEquiv, map_mul' := ⋯ }

theorem CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F A) (MulOpposite.unop ((CategoryTheory.PreGaloisCategory.endMulEquivAutGalois F) f))).hom A.pt = f.app A.obj A.pt

theorem CategoryTheory.PreGaloisCategory.FibreFunctor.end_isUnit {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) : IsUnit f

Any endomorphism of a fiber functor is a unit.

instance CategoryTheory.PreGaloisCategory.FibreFunctor.end_isIso {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) : CategoryTheory.IsIso f

Any endomorphism of a fiber functor is an isomorphism.

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.PreGaloisCategory.autMulEquivAutGalois {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Aut F ≃* (CategoryTheory.PreGaloisCategory.AutGalois F)ᵐᵒᵖ

The automorphism group of F is multiplicatively isomorphic to (the multiplicative opposite of) the limit over the automorphism groups of the Galois objects.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.Aut F) (A : C) [CategoryTheory.PreGaloisCategory.IsGalois A] (a : ↑(F.obj A)) : F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop ((CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F) f))).hom a = f.hom.app A a

@[simp]

theorem CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (x : CategoryTheory.PreGaloisCategory.AutGalois F) (A : C) [CategoryTheory.PreGaloisCategory.IsGalois A] (a : ↑(F.obj A)) : ((CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F).symm { unop' := x }).hom.app A a = F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom a

theorem CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isGalois {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] : MulAction.IsPretransitive (CategoryTheory.Aut F) ↑(F.obj X)

The Aut F action on the fiber of a Galois object is transitive. See pretransitive_of_isConnected for the same result for connected objects.

instance CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : MulAction.IsPretransitive (CategoryTheory.Aut F) ↑(F.obj X)

The Aut F action on the fiber of a connected object is transitive.

Equations

• ⋯ = ⋯