Theorems · Definition · category theory

CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj

{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} → CategoryTheory.PreGaloisCategory.PointedGaloisObject F → C

The underlying object of C.

Defined in: Mathlib.CategoryTheory.Galois.Prorepresentability
Cited by: 29 results in Mathlib
Foundations: Depth 13 from the axioms · uses propext
Assumes: CategoryTheory.Category CategoryTheory.GaloisCategory

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functorstatement and proof · cited by 16,252
Finitestatement · cited by 3,029
FintypeCatstatement and proof · cited by 217
CategoryTheory.GaloisCategorystatement and proof · cited by 88
CategoryTheory.PreGaloisCategory.PointedGaloisObjectstatement and proof · cited by 34

Cited by40

Results whose statement or proof uses this declaration.

CategoryTheory.PreGaloisCategory.PointedGaloisObject.ptstatement · cited by 16
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.valstatement · cited by 11
CategoryTheory.PreGaloisCategory.AutGalois.πstatement · cited by 9
CategoryTheory.PreGaloisCategory.PointedGaloisObject.inclproof · cited by 6
CategoryTheory.PreGaloisCategory.autGaloisSystemproof · cited by 6
CategoryTheory.PreGaloisCategory.endEquivAutGalois_πstatement and proof · cited by 3
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.extstatement and proof · cited by 2
CategoryTheory.PreGaloisCategory.PointedGaloisObject.comp_valstatement · cited by 1
CategoryTheory.PreGaloisCategory.PointedGaloisObject.hom_extstatement · cited by 1
CategoryTheory.PreGaloisCategory.autGaloisSystem_mapstatement · cited by 1
CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjectiveproof · cited by 1
CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizersstatement · cited by 1