Documentation Verification Report

Decomposition

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

Statistics

Metric	Count
Definitions	0
Theorems `connected_component_unique`, `exists_galois_representative`, `exists_hom_from_galois_of_connected`, `exists_hom_from_galois_of_fiber`, `exists_hom_from_galois_of_fiber_nonempty`, `fiber_in_connected_component`, `has_decomp_connected_components`, `has_decomp_connected_components'`, `natTrans_ext_of_isGalois`	9
Total	9

CategoryTheory.PreGaloisCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connected_component_unique` 📖	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`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `hasPullbacks` `not_initial_of_inhabited` `IsConnected.noTrivialComponent` `CategoryTheory.Limits.pullback.fst_of_mono` `CategoryTheory.Limits.pullback.snd_of_mono` `fiberPullbackEquiv_symm_fst_apply` `fiberPullbackEquiv_symm_snd_apply` `CategoryTheory.Functor.map_comp` `CategoryTheory.IsIso.hom_inv_id_assoc`
`exists_galois_representative` 📖	mathematical	—	`IsGalois` `Function.Bijective` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `DFunLike.coe` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `fiber_in_connected_component` `isGalois_iff_pretransitive` `CategoryTheory.Functor.map_comp` `DFunLike.congr_fun` `CategoryTheory.Iso.hom_inv_id` `evaluation_injective_of_isConnected`
`exists_hom_from_galois_of_connected` 📖	mathematical	—	`IsGalois`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `exists_hom_from_galois_of_fiber_nonempty` `nonempty_fiber_of_isConnected`
`exists_hom_from_galois_of_fiber` 📖	mathematical	—	`IsGalois` `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.GaloisCategory.toPreGaloisCategory` `exists_galois_representative` `Function.Bijective.surjective`
`exists_hom_from_galois_of_fiber_nonempty` 📖	mathematical	—	`IsGalois`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `exists_hom_from_galois_of_fiber`
`fiber_in_connected_component` 📖	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` `IsConnected` `CategoryTheory.Mono`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `has_decomp_connected_components` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts` `FiberFunctor.preservesFiniteCoproducts` `CategoryTheory.Limits.Concrete.isColimit_exists_rep` `CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit` `CategoryTheory.instFiniteDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.Limits.Types.hasColimit` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `instMonoCoprod` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `hasFiniteCoproducts` `Subtype.finite`
`has_decomp_connected_components` 📖	mathematical	—	`IsConnected` `Finite`	—	`instFiberFunctorGetFiberFunctor`
`has_decomp_connected_components'` 📖	mathematical	—	`IsConnected`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `hasFiniteCoproducts` `CategoryTheory.GaloisCategory.toPreGaloisCategory` `has_decomp_connected_components`
`natTrans_ext_of_isGalois` 📖	—	`CategoryTheory.NatTrans.app` `FintypeCat` `FintypeCat.instCategory`	—	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `CategoryTheory.NatTrans.ext'` `FintypeCat.hom_ext` `exists_hom_from_galois_of_fiber` `FunctorToFintypeCat.naturality`

---

← Back to Index