Theorems · Inductive type · category theory

CategoryTheory.PreGaloisCategory.PointedGaloisObject

{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [CategoryTheory.GaloisCategory C] → CategoryTheory.Functor C FintypeCat → Type (max u₁ u₂ w)

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

Defined in

Mathlib.CategoryTheory.Galois.Prorepresentability

Cited by

34 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategory