CategoryTheory.PreGaloisCategory.relativeDeck_isPretransitive
Original deck transitivity restricts to every fiber of an intermediate morphism. The relative deck transformations are actual over-category isomorphisms.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategoryLean source · statement
theorem relativeDeck_isPretransitive
{C : Type u} [Category.{v} C] [GaloisCategory C]
(F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
{A B : C} [IsGalois A] (f : A ⟶ B) (y : F.obj B) :
MulAction.IsPretransitive (Aut (Over.mk f))
((fiberOver F y).obj (Over.mk f))