Theorems · Inductive type · category theory
CategoryTheory.PreGaloisCategory.FiberFunctor
{C : Type u₁} →
[inst : CategoryTheory.Category.{u₂, u₁} C] →
[CategoryTheory.PreGaloisCategory C] → CategoryTheory.Functor C FintypeCat → PropDefinition of a fiber functor from a Galois category. Lenstra, Def 3.1, (G4)-(G6)
- Defined in
- Mathlib.CategoryTheory.Galois.Basic
- Cited by
- 66 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.Functorstatement · cited by 16,252
- Finitestatement · cited by 3,029
- FintypeCatstatement · cited by 217
- CategoryTheory.PreGaloisCategorystatement · cited by 21
Cited by84
Results whose statement or proof uses this declaration.
- CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGaloisstatement and proof · cited by 6
- CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnectedstatement and proof · cited by 6
- CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnectedstatement and proof · cited by 6
- CategoryTheory.PreGaloisCategory.autMulEquivAutGaloisstatement and proof · cited by 4
- CategoryTheory.PreGaloisCategory.endEquivAutGaloisstatement and proof · cited by 3
- CategoryTheory.PreGaloisCategory.endEquivAutGalois_πstatement and proof · cited by 3
- CategoryTheory.PreGaloisCategory.endMulEquivAutGaloisstatement and proof · cited by 3
- CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiberstatement and proof · cited by 3
- CategoryTheory.PreGaloisCategory.fiberBinaryProductEquivstatement and proof · cited by 3
- CategoryTheory.PreGaloisCategory.fiberPullbackEquivstatement and proof · cited by 3
- CategoryTheory.PreGaloisCategory.not_initial_of_inhabitedstatement and proof · cited by 3
- CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnectedstatement and proof · cited by 3