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 CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	CategoryTheory.Iso DFunLike.coe CategoryTheory.Functor.obj FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike 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	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types Finite CategoryTheory.Functor.obj FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category IsGalois Function.Bijective Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	—	CategoryTheory.GaloisCategory.toPreGaloisCategory fiber_in_connected_component isGalois_iff_pretransitive CategoryTheory.Functor.map_comp CategoryTheory.ConcreteCategory.congr_hom CategoryTheory.Iso.hom_inv_id evaluation_injective_of_isConnected
exists_hom_from_galois_of_connected 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct IsGalois	—	CategoryTheory.GaloisCategory.toPreGaloisCategory exists_hom_from_galois_of_fiber_nonempty nonempty_fiber_of_isConnected
exists_hom_from_galois_of_fiber 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types Finite CategoryTheory.Functor.obj FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category IsGalois DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype CategoryTheory.Functor.map	—	CategoryTheory.GaloisCategory.toPreGaloisCategory exists_galois_representative Function.Bijective.surjective
exists_hom_from_galois_of_fiber_nonempty 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct IsGalois	—	CategoryTheory.GaloisCategory.toPreGaloisCategory exists_hom_from_galois_of_fiber
fiber_in_connected_component 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types Finite CategoryTheory.Functor.obj FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Types.instFunLike 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	—	CategoryTheory.Limits.IsColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor IsConnected Finite	—	instFiberFunctorGetFiberFunctor
has_decomp_connected_components' 📖	mathematical	—	Finite CategoryTheory.Iso CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.Discrete.functor IsConnected	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts CategoryTheory.GaloisCategory.toPreGaloisCategory has_decomp_connected_components
natTrans_ext_of_isGalois 📖	—	CategoryTheory.NatTrans.app FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite	—	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.NatTrans.ext' FintypeCat.hom_ext exists_hom_from_galois_of_fiber FunctorToFintypeCat.naturality

---

← Back to Index