Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi

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

Defined in

Mathlib.CategoryTheory.Galois.Prorepresentability

Cited by

0 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctor