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.

References #

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

source

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

Type (max u₁ u₂)

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.

Instances For

source

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.

source

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 }

source

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

source

theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.ext {C : Type u₁} :

source

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.

Instances For

source

@[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.

source

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 u₂ u₁} (CategoryTheory.PreGaloisCategory.PointedGaloisObject F)

The category of pointed Galois objects.

Equations

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

source

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 }

source

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

source

@[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

source

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)

source

@[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

source

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

⋯ = ⋯

source

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.

Instances For

source

@[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

source

@[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

source

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.

Instances For

source

@[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 { unop := A }).app B f = F.map f A.pt

source

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.

Instances For

source

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

⋯ = ⋯

source

@[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

source

@[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)

source

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.

Instances For

source

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

Instances For

source

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)

source

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

Instances For

source

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

source

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)

source

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.

source

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.

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 (slighty 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.

source

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.

Instances For

source

@[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

source

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.

Instances For

source

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

source

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.

Instances For

source

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

source

@[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

source

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' := ⋯ }

Instances For

source

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

source

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.

source

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

⋯ = ⋯

source

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