Theorems · Theorem · category theory
CategoryTheory.PreGaloisCategory.autGaloisSystem_map
∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
(F : CategoryTheory.Functor C FintypeCat) {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : A ⟶ B),
(CategoryTheory.PreGaloisCategory.autGaloisSystem F).map f =
GrpCat.ofHom (CategoryTheory.PreGaloisCategory.autMapHom f.val)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
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
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Functor.mapstatement and proof · cited by 8,698
- Finitestatement · cited by 3,029
- FintypeCatstatement and proof · cited by 217
- GrpCatstatement · cited by 146
- CategoryTheory.Autstatement · cited by 96
- CategoryTheory.GaloisCategorystatement and proof · cited by 88
- CategoryTheory.PreGaloisCategory.PointedGaloisObjectstatement and proof · cited by 34
- GrpCat.ofstatement · cited by 32
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.objstatement · cited by 29
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjectiveproof · cited by 1