Documentation Verification Report

GaloisObjects

📁 Source: Mathlib/CategoryTheory/Galois/GaloisObjects.lean

Statistics

Metric	Count
Definitions `IsGalois`, `autMap`, `autMapHom`, `autMulFiber`, `evaluationEquivOfIsGalois`, `isTerminalQuotientOfIsGalois`, `quotientByAutTerminalEquivUniqueQuotient`	7
Theorems `quotientByAutTerminal`, `toIsConnected`, `autMapHom_apply`, `autMap_apply_mul`, `autMap_comp`, `autMap_id`, `autMap_surjective_of_isGalois`, `autMap_unique`, `comp_autMap`, `comp_autMap_apply`, `evaluationEquivOfIsGalois_apply`, `evaluationEquivOfIsGalois_symm_fiber`, `evaluation_aut_bijective_of_isGalois`, `evaluation_aut_surjective_of_isGalois`, `exists_autMap`, `instPreservesColimitsOfShapeFintypeCatSingleObjInclOfFinite`, `isGalois_iff_aux`, `isGalois_iff_pretransitive`, `isPretransitive_of_isGalois`, `stabilizer_normal_of_isGalois`	20
Total	27

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
`IsGalois` 📖	CompData	8 math math: `isGalois_iff_aux`, `PointedGaloisObject.isGalois`, `autMulEquivAutGalois_symm_app`, `exists_hom_from_galois_of_connected`, `exists_hom_from_galois_of_fiber_nonempty`, `exists_hom_from_galois_of_fiber`, `isGalois_iff_pretransitive`, `exists_galois_representative`
`autMap` 📖	CompOp	8 math math: `autMap_comp`, `autMapHom_apply`, `comp_autMap`, `autMap_surjective_of_isGalois`, `autMap_apply_mul`, `autMap_unique`, `comp_autMap_apply`, `autMap_id`
`autMapHom` 📖	CompOp	2 math math: `autMapHom_apply`, `autGaloisSystem_map`
`autMulFiber` 📖	CompOp	2 math math: `isGalois_iff_pretransitive`, `isPretransitive_of_isGalois`
`evaluationEquivOfIsGalois` 📖	CompOp	3 math math: `autIsoFibers_inv_app`, `evaluationEquivOfIsGalois_apply`, `evaluationEquivOfIsGalois_symm_fiber`
`isTerminalQuotientOfIsGalois` 📖	CompOp	—
`quotientByAutTerminalEquivUniqueQuotient` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`autMapHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CategoryTheory.Aut` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `autMapHom` `autMap`	—	—
`autMap_apply_mul` 📖	mathematical	—	`autMap` `CategoryTheory.Aut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup`	—	`nonempty_fiber_of_isConnected` `CategoryTheory.GaloisCategory.toPreGaloisCategory` `instFiberFunctorGetFiberFunctor` `evaluation_aut_injective_of_isConnected` `IsGalois.toIsConnected` `comp_autMap_apply` `CategoryTheory.Functor.map_comp` `CategoryTheory.comp_apply`
`autMap_comp` 📖	mathematical	—	`autMap` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Aut` `IsGalois.toIsConnected`	—	`IsGalois.toIsConnected` `autMap_unique` `CategoryTheory.Category.assoc` `comp_autMap`
`autMap_id` 📖	mathematical	—	`autMap` `IsGalois.toIsConnected` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Aut`	—	`IsGalois.toIsConnected` `autMap_unique` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`autMap_surjective_of_isGalois` 📖	mathematical	—	`CategoryTheory.Aut` `autMap` `IsGalois.toIsConnected`	—	`IsGalois.toIsConnected` `nonempty_fiber_of_isConnected` `CategoryTheory.GaloisCategory.toPreGaloisCategory` `instFiberFunctorGetFiberFunctor` `surjective_of_nonempty_fiber_of_isConnected` `MulAction.exists_smul_eq` `isPretransitive_of_isGalois` `evaluation_aut_injective_of_isConnected` `comp_autMap_apply`
`autMap_unique` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom`	`autMap`	—	`exists_autMap`
`comp_autMap` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom` `autMap`	—	`exists_autMap`
`comp_autMap_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `autMap`	—	`CategoryTheory.Functor.map_comp` `DFunLike.congr_fun` `CategoryTheory.Functor.congr_map` `comp_autMap`
`evaluationEquivOfIsGalois_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Aut` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `EquivLike.toFunLike` `Equiv.instEquivLike` `evaluationEquivOfIsGalois` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory`
`evaluationEquivOfIsGalois_symm_fiber` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `Equiv` `CategoryTheory.Aut` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `evaluationEquivOfIsGalois`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `Equiv.apply_symm_apply`
`evaluation_aut_bijective_of_isGalois` 📖	mathematical	—	`Function.Bijective` `CategoryTheory.Aut` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `DFunLike.coe` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `evaluation_aut_injective_of_isConnected` `IsGalois.toIsConnected` `evaluation_aut_surjective_of_isGalois`
`evaluation_aut_surjective_of_isGalois` 📖	mathematical	—	`CategoryTheory.Aut` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `DFunLike.coe` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `MulAction.IsPretransitive.exists_smul_eq` `isPretransitive_of_isGalois`
`exists_autMap` 📖	mathematical	—	`ExistsUnique` `CategoryTheory.Aut` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Iso.hom`	—	`nonempty_fiber_of_isConnected` `CategoryTheory.GaloisCategory.toPreGaloisCategory` `instFiberFunctorGetFiberFunctor` `evaluation_injective_of_isConnected` `CategoryTheory.Functor.map_comp` `CategoryTheory.comp_apply` `evaluationEquivOfIsGalois_symm_fiber` `evaluation_aut_injective_of_isConnected` `IsGalois.toIsConnected` `DFunLike.congr_fun` `CategoryTheory.Functor.congr_map`
`instPreservesColimitsOfShapeFintypeCatSingleObjInclOfFinite` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.types` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FintypeCat.incl`	—	`CategoryTheory.Limits.preservesColimitsOfShape_of_equiv` `CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits` `CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteColimits` `Finite.exists_type_univ_nonempty_mulEquiv`
`isGalois_iff_aux` 📖	mathematical	—	`IsGalois` `CategoryTheory.Limits.IsTerminal` `CategoryTheory.Limits.colimit` `CategoryTheory.SingleObj` `CategoryTheory.Aut` `CategoryTheory.SingleObj.category` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `CategoryTheory.SingleObj.functor` `CategoryTheory.Aut.toEnd` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instHasColimitsOfShapeSingleObjOfFinite` `CategoryTheory.GaloisCategory.toPreGaloisCategory` `instFiniteAutOfIsConnected`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instHasColimitsOfShapeSingleObjOfFinite` `CategoryTheory.GaloisCategory.toPreGaloisCategory` `instFiniteAutOfIsConnected` `IsGalois.quotientByAutTerminal`
`isGalois_iff_pretransitive` 📖	mathematical	—	`IsGalois` `MulAction.IsPretransitive` `CategoryTheory.Aut` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MulAction.toSemigroupAction` `autMulFiber`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instHasColimitsOfShapeSingleObjOfFinite` `instFiniteAutOfIsConnected` `isGalois_iff_aux` `Equiv.nonempty_congr` `MulAction.pretransitive_iff_unique_quotient_of_nonempty` `nonempty_fiber_of_isConnected`
`isPretransitive_of_isGalois` 📖	mathematical	—	`MulAction.IsPretransitive` `CategoryTheory.Aut` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MulAction.toSemigroupAction` `autMulFiber`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `isGalois_iff_pretransitive` `IsGalois.toIsConnected`
`stabilizer_normal_of_isGalois` 📖	mathematical	—	`Subgroup.Normal` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `CategoryTheory.Aut.instGroup` `MulAction.stabilizer` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `instMulActionAutFunctorFintypeCatCarrierObj`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `MulAction.mem_stabilizer_iff` `MulAction.IsPretransitive.exists_smul_eq` `isPretransitive_of_isGalois` `mulAction_naturality` `smul_inv_smul`

CategoryTheory.PreGaloisCategory.IsGalois

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quotientByAutTerminal` 📖	mathematical	—	`CategoryTheory.Limits.IsTerminal` `CategoryTheory.Limits.colimit` `CategoryTheory.SingleObj` `CategoryTheory.Aut` `CategoryTheory.SingleObj.category` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `CategoryTheory.SingleObj.functor` `CategoryTheory.Aut.toEnd` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.PreGaloisCategory.instHasColimitsOfShapeSingleObjOfFinite` `CategoryTheory.GaloisCategory.toPreGaloisCategory` `CategoryTheory.PreGaloisCategory.instFiniteAutOfIsConnected` `toIsConnected`	—	—
`toIsConnected` 📖	mathematical	—	`CategoryTheory.PreGaloisCategory.IsConnected`	—	—

---

← Back to Index