Documentation Verification Report

Prorepresentability

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

Statistics

Metric	Count
Definitions `AutGalois`, `π`, `PointedGaloisObject`, `val`, `cocone`, `incl`, `instCategory`, `instCoeDep`, `instCoeHomHomObj`, `isColimit`, `obj`, `pt`, `autGaloisSystem`, `autIsoFibers`, `autMulEquivAutGalois`, `endEquivAutGalois`, `endEquivSectionsFibers`, `endMulEquivAutGalois`, `instGroupAutGalois`	19
Theorems `ext`, `π_apply`, `π_surjective`, `isPretransitive_of_isConnected`, `isPretransitive_of_isGalois`, `end_isIso`, `end_isUnit`, `comp`, `ext`, `ext_iff`, `cocone_app`, `comp_val`, `comp_val_assoc`, `hom_ext`, `hom_ext_iff`, `id_val`, `incl_map`, `incl_obj`, `instHasColimitOppositeFunctorTypeCompOpInclCoyoneda`, `instIsCofilteredOrEmpty`, `isGalois`, `autGaloisSystem_map`, `autGaloisSystem_map_surjective`, `autGaloisSystem_obj_coe`, `autIsoFibers_inv_app`, `autMulEquivAutGalois_symm_app`, `autMulEquivAutGalois_π`, `endEquivAutGalois_mul`, `endEquivAutGalois_π`, `endEquivSectionsFibers_π`, `endMulEquivAutGalois_pi`	31
Total	50

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
`AutGalois` 📖	CompOp	7 math math: `autMulEquivAutGalois_symm_app`, `autMulEquivAutGalois_π`, `endEquivAutGalois_mul`, `AutGalois.π_apply`, `endEquivAutGalois_π`, `AutGalois.π_surjective`, `endMulEquivAutGalois_pi`
`PointedGaloisObject` 📖	CompData	15 math math: `endEquivSectionsFibers_π`, `PointedGaloisObject.incl_obj`, `autIsoFibers_inv_app`, `PointedGaloisObject.instIsCofilteredOrEmpty`, `nhds_one_has_basis_stabilizers`, `PointedGaloisObject.incl_map`, `PointedGaloisObject.comp_val`, `AutGalois.π_apply`, `PointedGaloisObject.instHasColimitOppositeFunctorTypeCompOpInclCoyoneda`, `PointedGaloisObject.comp_val_assoc`, `autGaloisSystem_map`, `PointedGaloisObject.cocone_app`, `autGaloisSystem_map_surjective`, `autGaloisSystem_obj_coe`, `PointedGaloisObject.id_val`
`autGaloisSystem` 📖	CompOp	5 math math: `autIsoFibers_inv_app`, `AutGalois.π_apply`, `autGaloisSystem_map`, `autGaloisSystem_map_surjective`, `autGaloisSystem_obj_coe`
`autIsoFibers` 📖	CompOp	1 math math: `autIsoFibers_inv_app`
`autMulEquivAutGalois` 📖	CompOp	2 math math: `autMulEquivAutGalois_symm_app`, `autMulEquivAutGalois_π`
`endEquivAutGalois` 📖	CompOp	2 math math: `endEquivAutGalois_mul`, `endEquivAutGalois_π`
`endEquivSectionsFibers` 📖	CompOp	1 math math: `endEquivSectionsFibers_π`
`endMulEquivAutGalois` 📖	CompOp	1 math math: `endMulEquivAutGalois_pi`
`instGroupAutGalois` 📖	CompOp	7 math math: `autMulEquivAutGalois_symm_app`, `autMulEquivAutGalois_π`, `endEquivAutGalois_mul`, `AutGalois.π_apply`, `endEquivAutGalois_π`, `AutGalois.π_surjective`, `endMulEquivAutGalois_pi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`autGaloisSystem_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `PointedGaloisObject` `PointedGaloisObject.instCategory` `GrpCat` `GrpCat.instCategory` `autGaloisSystem` `GrpCat.ofHom` `CategoryTheory.Aut` `PointedGaloisObject.obj` `CategoryTheory.Aut.instGroup` `autMapHom` `PointedGaloisObject.isGalois` `PointedGaloisObject.Hom.val`	—	—
`autGaloisSystem_map_surjective` 📖	mathematical	—	`GrpCat.carrier` `CategoryTheory.Functor.obj` `PointedGaloisObject` `PointedGaloisObject.instCategory` `GrpCat` `GrpCat.instCategory` `autGaloisSystem` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MonoidHom.instFunLike` `GrpCat.instConcreteCategoryMonoidHomCarrier` `CategoryTheory.Functor.map`	—	`IsGalois.toIsConnected` `PointedGaloisObject.isGalois` `autMap_surjective_of_isGalois`
`autGaloisSystem_obj_coe` 📖	mathematical	—	`GrpCat.carrier` `CategoryTheory.Functor.obj` `PointedGaloisObject` `PointedGaloisObject.instCategory` `GrpCat` `GrpCat.instCategory` `autGaloisSystem` `CategoryTheory.Aut` `PointedGaloisObject.obj`	—	—
`autIsoFibers_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `PointedGaloisObject` `PointedGaloisObject.instCategory` `CategoryTheory.types` `CategoryTheory.Functor.comp` `PointedGaloisObject.incl` `FintypeCat` `FintypeCat.instCategory` `FintypeCat.incl` `GrpCat` `GrpCat.instCategory` `autGaloisSystem` `CategoryTheory.forget` `MonoidHom` `GrpCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MonoidHom.instFunLike` `GrpCat.instConcreteCategoryMonoidHomCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `autIsoFibers` `DFunLike.coe` `Equiv` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `PointedGaloisObject.obj` `CategoryTheory.Aut` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `evaluationEquivOfIsGalois` `PointedGaloisObject.isGalois` `PointedGaloisObject.pt`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory`
`autMulEquivAutGalois_symm_app` 📖	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.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `MulEquiv` `MulOpposite` `AutGalois` `CategoryTheory.Aut` `MulOpposite.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupAutGalois` `CategoryTheory.Aut.instGroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `autMulEquivAutGalois` `PreOpposite.op'` `PointedGaloisObject.obj` `IsGalois` `CategoryTheory.Functor.map` `MonoidHom` `MonoidHom.instFunLike` `AutGalois.π`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `autMulEquivAutGalois_π` `MulEquiv.apply_symm_apply`
`autMulEquivAutGalois_π` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `PointedGaloisObject.obj` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `MonoidHom` `AutGalois` `CategoryTheory.Aut` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupAutGalois` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `AutGalois.π` `MulOpposite.unop` `MulEquiv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `MulOpposite` `MulOne.toMul` `MulOpposite.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `autMulEquivAutGalois` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `endEquivAutGalois_π`
`endEquivAutGalois_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.End` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `AutGalois` `EquivLike.toFunLike` `Equiv.instEquivLike` `endEquivAutGalois` `CategoryTheory.CategoryStruct.comp` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupAutGalois`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `AutGalois.ext` `evaluation_aut_injective_of_isConnected` `IsGalois.toIsConnected` `PointedGaloisObject.isGalois` `endEquivAutGalois_π` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `CategoryTheory.Functor.map_comp` `CategoryTheory.NatTrans.naturality` `FintypeCat.comp_apply`
`endEquivAutGalois_π` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `PointedGaloisObject.obj` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `MonoidHom` `AutGalois` `CategoryTheory.Aut` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupAutGalois` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `AutGalois.π` `Equiv` `CategoryTheory.End` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `endEquivAutGalois` `PointedGaloisObject.pt` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `PointedGaloisObject.isGalois` `endEquivSectionsFibers_π` `evaluationEquivOfIsGalois_symm_fiber`
`endEquivSectionsFibers_π` 📖	mathematical	—	`Set` `Set.instMembership` `CategoryTheory.Functor.sections` `PointedGaloisObject` `PointedGaloisObject.instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.types` `PointedGaloisObject.incl` `FintypeCat` `FintypeCat.instCategory` `FintypeCat.incl` `DFunLike.coe` `Equiv` `CategoryTheory.End` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `endEquivSectionsFibers` `CategoryTheory.Functor.obj` `PointedGaloisObject.obj` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `FintypeCat.concreteCategoryFintype` `CategoryTheory.NatTrans.app` `PointedGaloisObject.pt`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `PointedGaloisObject.instHasColimitOppositeFunctorTypeCompOpInclCoyoneda` `FintypeCat.instFullIncl` `FintypeCat.instFaithfulIncl` `CategoryTheory.Limits.Types.limitEquivSections_apply` `CategoryTheory.Limits.colimitCoyonedaHomIsoLimit'_π_apply` `CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom` `CategoryTheory.Functor.map_id` `CategoryTheory.id_apply`
`endMulEquivAutGalois_pi` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `PointedGaloisObject.obj` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `MonoidHom` `AutGalois` `CategoryTheory.Aut` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupAutGalois` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `AutGalois.π` `MulOpposite.unop` `MulEquiv` `CategoryTheory.End` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `MulOpposite` `CategoryTheory.End.mul` `MulOpposite.instMul` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `endMulEquivAutGalois` `PointedGaloisObject.pt` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `endEquivAutGalois_π`

CategoryTheory.PreGaloisCategory.AutGalois

Definitions

Name	Category	Theorems
`π` 📖	CompOp	6 math math: `CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app`, `CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π`, `π_apply`, `CategoryTheory.PreGaloisCategory.endEquivAutGalois_π`, `π_surjective`, `CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`DFunLike.coe` `MonoidHom` `CategoryTheory.PreGaloisCategory.AutGalois` `CategoryTheory.Aut` `CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.PreGaloisCategory.instGroupAutGalois` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `π`	—	—	—
`π_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CategoryTheory.PreGaloisCategory.AutGalois` `CategoryTheory.Aut` `CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.PreGaloisCategory.instGroupAutGalois` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `π` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `CategoryTheory.PreGaloisCategory.PointedGaloisObject` `CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCategory` `CategoryTheory.Functor.comp` `GrpCat` `GrpCat.instCategory` `CategoryTheory.types` `CategoryTheory.PreGaloisCategory.autGaloisSystem` `CategoryTheory.forget` `GrpCat.carrier` `GrpCat.str` `GrpCat.instConcreteCategoryMonoidHomCarrier`	—	—
`π_surjective` 📖	mathematical	—	`CategoryTheory.PreGaloisCategory.AutGalois` `CategoryTheory.Aut` `CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.PreGaloisCategory.instGroupAutGalois` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `π`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `CategoryTheory.PreGaloisCategory.instFiniteAutOfIsConnected` `CategoryTheory.PreGaloisCategory.IsGalois.toIsConnected` `CategoryTheory.PreGaloisCategory.PointedGaloisObject.isGalois` `CategoryTheory.Functor.eval_section_surjective_of_surjective` `CategoryTheory.PreGaloisCategory.PointedGaloisObject.instIsCofilteredOrEmpty` `One.instNonempty` `CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective`

CategoryTheory.PreGaloisCategory.FiberFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPretransitive_of_isConnected` 📖	mathematical	—	`MulAction.IsPretransitive` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MulAction.toSemigroupAction` `CategoryTheory.PreGaloisCategory.instMulActionAutFunctorFintypeCatCarrierObj`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `MulAction.exists_smul_eq` `comp_right` `FintypeCat.instIsEquivalenceUSwitch` `FintypeCat.hom_ext` `FintypeCat.uSwitchEquiv_naturality` `CategoryTheory.Functor.comp_map` `FunctorToFintypeCat.naturality` `FintypeCat.uSwitchEquiv_symm_naturality` `Equiv.apply_symm_apply`
`isPretransitive_of_isGalois` 📖	mathematical	—	`MulAction.IsPretransitive` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MulAction.toSemigroupAction` `CategoryTheory.PreGaloisCategory.instMulActionAutFunctorFintypeCatCarrierObj`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `MulAction.IsPretransitive.exists_smul_eq` `CategoryTheory.PreGaloisCategory.isPretransitive_of_isGalois` `CategoryTheory.PreGaloisCategory.AutGalois.π_surjective` `CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app`

CategoryTheory.PreGaloisCategory.FibreFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`end_isIso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `CategoryTheory.isUnit_iff_isIso` `end_isUnit`
`end_isUnit` 📖	mathematical	—	`IsUnit` `CategoryTheory.End` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.End.monoid`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `isUnit_map_iff` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `isLocalHom_equiv` `Group.isUnit`

CategoryTheory.PreGaloisCategory.PointedGaloisObject

Definitions

Name	Category	Theorems
`cocone` 📖	CompOp	1 math math: `cocone_app`
`incl` 📖	CompOp	6 math math: `CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π`, `incl_obj`, `CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app`, `incl_map`, `instHasColimitOppositeFunctorTypeCompOpInclCoyoneda`, `cocone_app`
`instCategory` 📖	CompOp	14 math math: `CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π`, `incl_obj`, `CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app`, `instIsCofilteredOrEmpty`, `incl_map`, `comp_val`, `CategoryTheory.PreGaloisCategory.AutGalois.π_apply`, `instHasColimitOppositeFunctorTypeCompOpInclCoyoneda`, `comp_val_assoc`, `CategoryTheory.PreGaloisCategory.autGaloisSystem_map`, `cocone_app`, `CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective`, `CategoryTheory.PreGaloisCategory.autGaloisSystem_obj_coe`, `id_val`
`instCoeDep` 📖	CompOp	—
`instCoeHomHomObj` 📖	CompOp	—
`isColimit` 📖	CompOp	—
`obj` 📖	CompOp	18 math math: `CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π`, `incl_obj`, `isGalois`, `CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app`, `CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app`, `CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers`, `CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π`, `comp_val`, `Hom.comp`, `CategoryTheory.PreGaloisCategory.AutGalois.π_apply`, `CategoryTheory.PreGaloisCategory.endEquivAutGalois_π`, `comp_val_assoc`, `CategoryTheory.PreGaloisCategory.autGaloisSystem_map`, `CategoryTheory.PreGaloisCategory.AutGalois.π_surjective`, `cocone_app`, `CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi`, `CategoryTheory.PreGaloisCategory.autGaloisSystem_obj_coe`, `id_val`
`pt` 📖	CompOp	7 math math: `CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π`, `CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app`, `CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers`, `Hom.comp`, `CategoryTheory.PreGaloisCategory.endEquivAutGalois_π`, `cocone_app`, `CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocone_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.PreGaloisCategory.PointedGaloisObject` `CategoryTheory.Category.opposite` `instCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `incl` `CategoryTheory.coyoneda` `Opposite.op` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `cocone` `CategoryTheory.Limits.Cocone.ι` `DFunLike.coe` `FintypeCat` `FintypeCat.instCategory` `obj` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `pt`	—	—
`comp_val` 📖	mathematical	—	`Hom.val` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.PreGaloisCategory.PointedGaloisObject` `CategoryTheory.Category.toCategoryStruct` `instCategory` `obj`	—	—
`comp_val_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `Hom.val` `CategoryTheory.PreGaloisCategory.PointedGaloisObject` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_val`
`hom_ext` 📖	—	`Hom.val`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.val`	—	`hom_ext`
`id_val` 📖	mathematical	—	`Hom.val` `CategoryTheory.CategoryStruct.id` `CategoryTheory.PreGaloisCategory.PointedGaloisObject` `CategoryTheory.Category.toCategoryStruct` `instCategory` `obj`	—	—
`incl_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.PreGaloisCategory.PointedGaloisObject` `instCategory` `incl` `Hom.val`	—	—
`incl_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.PreGaloisCategory.PointedGaloisObject` `instCategory` `incl` `obj`	—	—
`instHasColimitOppositeFunctorTypeCompOpInclCoyoneda` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `Opposite` `CategoryTheory.PreGaloisCategory.PointedGaloisObject` `CategoryTheory.Category.opposite` `instCategory` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `incl` `CategoryTheory.coyoneda`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory`
`instIsCofilteredOrEmpty` 📖	mathematical	—	`CategoryTheory.IsCofilteredOrEmpty` `CategoryTheory.PreGaloisCategory.PointedGaloisObject` `instCategory`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.PreGaloisCategory.instHasBinaryProducts` `CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber` `CategoryTheory.Functor.map_comp` `CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply` `CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply` `hom_ext` `CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected` `CategoryTheory.PreGaloisCategory.IsGalois.toIsConnected` `CategoryTheory.comp_apply`
`isGalois` 📖	mathematical	—	`CategoryTheory.PreGaloisCategory.IsGalois` `obj`	—	—

CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom

Definitions

Name	Category	Theorems
`val` 📖	CompOp	8 math math: `CategoryTheory.PreGaloisCategory.PointedGaloisObject.hom_ext_iff`, `CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl_map`, `CategoryTheory.PreGaloisCategory.PointedGaloisObject.comp_val`, `ext_iff`, `comp`, `CategoryTheory.PreGaloisCategory.PointedGaloisObject.comp_val_assoc`, `CategoryTheory.PreGaloisCategory.autGaloisSystem_map`, `CategoryTheory.PreGaloisCategory.PointedGaloisObject.id_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `val` `CategoryTheory.PreGaloisCategory.PointedGaloisObject.pt`	—	—
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`

---

← Back to Index