Documentation Verification Report

Injective

📁 Source: Mathlib/Topology/Category/LightProfinite/Injective.lean

Statistics

Metric	Count
Definitions	0
Theorems `injective`, `exists_lift_of_finite_of_injective_of_surjective`, `exists_lift_of_finite_of_mono_of_epi`, `injective_of_finite`, `injective_of_light`	5
Total	5

LightProfinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective` 📖	mathematical	—	`CategoryTheory.Injective` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology`	—	`CategoryTheory.Injective.factors` `Profinite.injective_of_light` `CategoryTheory.Functor.map_mono` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape` `CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape` `CategoryTheory.instCountableCategoryOfFinCategory` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `Profinite.hasLimits` `CategoryTheory.Functor.FullyFaithful.map_injective` `CompHausLike.is_compact` `CompHausLike.is_hausdorff`

Profinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lift_of_finite_of_injective_of_surjective` 📖	—	`Continuous`	—	—	`Finite.of_surjective` `Topology.IsClosedEmbedding.isClosed_iff_image_isClosed` `Continuous.isClosedEmbedding` `IsClosed.preimage` `isClosed_singleton` `T2Space.t1Space` `Set.pairwiseDisjoint_iff` `IsClopen.preimage` `isClopen_discrete` `Finite.instDiscreteTopology` `Set.mem_preimage` `Set.mem_singleton_iff` `Set.mem_image` `exists_clopen_partition_of_clopen_cover` `Set.univ_subset_iff` `subset_trans` `Set.instIsTransSubset` `IsLocallyConstant.continuous` `IsLocallyConstant.iff_isOpen_fiber` `Set.ext` `Set.preimage_liftCover` `Set.mem_iUnion` `Set.liftCover_of_mem` `symm` `IsEquiv.toSymm` `eq_isEquiv`
`exists_lift_of_finite_of_mono_of_epi` 📖	—	`CategoryTheory.CategoryStruct.comp` `Profinite` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str`	—	—	`exists_lift_of_finite_of_injective_of_surjective` `CompHausLike.is_compact` `CompHausLike.is_hausdorff` `instTotallyDisconnectedSpaceCarrierToTop` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `CompHausLike.mono_iff_injective` `epi_iff_surjective` `instHasPropTotallyDisconnectedSpaceCarrier` `CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext` `CategoryTheory.comp_apply`
`injective_of_finite` 📖	mathematical	—	`CategoryTheory.Injective` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str`	—	`Finite.compactSpace` `Finite.of_fintype` `DiscreteTopology.toT2Space` `instDiscreteTopologyPUnit` `instHasPropTotallyDisconnectedSpaceCarrier` `TotallySeparatedSpace.totallyDisconnectedSpace` `TotallySeparatedSpace.of_discrete` `CategoryTheory.IsSplitEpi.mk'` `exists_lift_of_finite_of_mono_of_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsRegularEpi` `CategoryTheory.instIsRegularEpiOfIsSplitEpi` `CategoryTheory.Limits.IsTerminal.hom_ext`
`injective_of_light` 📖	mathematical	—	`CategoryTheory.Injective` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.obj` `LightProfinite` `SecondCountableTopology` `lightToProfinite`	—	`Finite.of_fintype` `Nonempty.map` `LightProfinite.epi_iff_surjective` `LightProfinite.surjective_transitionMap` `CategoryTheory.Injective.factors` `injective_of_finite` `CategoryTheory.Functor.map_comp` `LightProfinite.proj_comp_transitionMap` `exists_lift_of_finite_of_mono_of_epi` `CategoryTheory.Functor.map_epi` `LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite` `Subtype.prop` `CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit` `CategoryTheory.countableCategoryOpposite` `CategoryTheory.instCountableCategoryNat` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `hasLimits` `CategoryTheory.Limits.IsLimit.uniq` `CompHausLike.is_compact` `CompHausLike.is_hausdorff` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.IsLimit.fac`

---

← Back to Index