Documentation Verification Report

InternallyProjective

📁 Source: Mathlib/Condensed/Light/InternallyProjective.lean

Statistics

Metric	Count
Definitions `InternallyProjective`, `ihomPoints`	2
Theorems `free_internallyProjective_iff_tensor_condition`, `free_internallyProjective_iff_tensor_condition'`, `free_lightProfinite_internallyProjective_iff_tensor_condition`, `free_lightProfinite_internallyProjective_iff_tensor_condition'`, `ihomPoints_apply`, `ihomPoints_symm_apply`, `ihomPoints_symm_comp`, `ihom_map_val_app`, `internallyProjective_iff_tensor_condition`, `internallyProjective_iff_tensor_condition'`	10
Total	12

CategoryTheory

Definitions

Name	Category	Theorems
`InternallyProjective` 📖	MathDef	7 math math: `LightCondensed.free_internallyProjective_iff_tensor_condition`, `LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition`, `LightCondensed.internallyProjective_iff_tensor_condition`, `LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition'`, `LightCondensed.free_internallyProjective_iff_tensor_condition'`, `InternallyProjective.ofRetract`, `LightCondensed.internallyProjective_iff_tensor_condition'`

LightCondensed

Definitions

Name	Category	Theorems
`ihomPoints` 📖	CompOp	4 math math: `ihomPoints_apply`, `ihomPoints_symm_comp`, `ihomPoints_symm_apply`, `ihom_map_val_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`free_internallyProjective_iff_tensor_condition` 📖	mathematical	—	`CategoryTheory.InternallyProjective` `LightCondMod` `CommRing.toRing` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryLightCondMod` `instMonoidalClosedLightCondMod` `CategoryTheory.Functor.obj` `LightCondSet` `CategoryTheory.types` `free` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instCartesianMonoidalCategoryLightCondSet` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `lightProfiniteToLightCondSet` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `LightProfinite.toCondensed`	—	`internallyProjective_iff_tensor_condition` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.OplaxMonoidal.δ_natural_right` `CategoryTheory.Functor.Monoidal.δ_μ` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.Monoidal.μ_δ`
`free_internallyProjective_iff_tensor_condition'` 📖	mathematical	—	`CategoryTheory.InternallyProjective` `LightCondMod` `CommRing.toRing` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryLightCondMod` `instMonoidalClosedLightCondMod` `CategoryTheory.Functor.obj` `LightCondSet` `CategoryTheory.types` `free` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instCartesianMonoidalCategoryLightCondSet` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `lightProfiniteToLightCondSet` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `LightProfinite.toCondensed`	—	`internallyProjective_iff_tensor_condition'` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc` `CategoryTheory.Functor.Monoidal.δ_μ_assoc` `CategoryTheory.Functor.Monoidal.μ_δ` `CategoryTheory.Category.comp_id`
`free_lightProfinite_internallyProjective_iff_tensor_condition` 📖	mathematical	—	`CategoryTheory.InternallyProjective` `LightCondMod` `CommRing.toRing` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryLightCondMod` `instMonoidalClosedLightCondMod` `CategoryTheory.Functor.obj` `LightCondSet` `CategoryTheory.types` `free` `LightProfinite.toCondensed` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `lightProfiniteToLightCondSet` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `LightProfinite.instCartesianMonoidalCategory` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	`free_internallyProjective_iff_tensor_condition` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.LaxMonoidal.μ_natural_right` `CategoryTheory.Functor.Monoidal.δ_μ_assoc` `CategoryTheory.Functor.Monoidal.μ_δ` `CategoryTheory.Category.comp_id`
`free_lightProfinite_internallyProjective_iff_tensor_condition'` 📖	mathematical	—	`CategoryTheory.InternallyProjective` `LightCondMod` `CommRing.toRing` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryLightCondMod` `instMonoidalClosedLightCondMod` `CategoryTheory.Functor.obj` `LightCondSet` `CategoryTheory.types` `free` `LightProfinite.toCondensed` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `lightProfiniteToLightCondSet` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `LightProfinite.instCartesianMonoidalCategory` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	`free_internallyProjective_iff_tensor_condition'` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.LaxMonoidal.μ_natural_left` `CategoryTheory.Functor.Monoidal.δ_μ_assoc` `CategoryTheory.Functor.Monoidal.μ_δ` `CategoryTheory.Category.comp_id`
`ihomPoints_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.Functor.obj` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `LightCondMod` `instCategoryLightCondensed` `CategoryTheory.ihom` `instMonoidalCategoryLightCondMod` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosedLightCondMod` `Opposite.op` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `LightCondSet` `CategoryTheory.types` `free` `LightProfinite.toCondensed` `EquivLike.toFunLike` `Equiv.instEquivLike` `ihomPoints` `CategoryTheory.MonoidalClosed.uncurry` `CategoryTheory.Sheaf` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `LightProfinite.instPreregular` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.GrothendieckTopology.yoneda` `CategoryTheory.coherentTopology.subcanonical` `forget` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv` `freeForgetAdjunction` `CategoryTheory.GrothendieckTopology.yonedaEquiv`	—	—
`ihomPoints_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `LightCondMod` `CommRing.toRing` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryLightCondMod` `CategoryTheory.Functor.obj` `LightCondSet` `CategoryTheory.types` `free` `LightProfinite.toCondensed` `ModuleCat.carrier` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.ihom` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosedLightCondMod` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ihomPoints` `CategoryTheory.Sheaf` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `LightProfinite.instPreregular` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.GrothendieckTopology.yoneda` `CategoryTheory.coherentTopology.subcanonical` `forget` `CategoryTheory.GrothendieckTopology.yonedaEquiv` `CategoryTheory.Adjunction.homEquiv` `freeForgetAdjunction` `CategoryTheory.MonoidalClosed.curry`	—	—
`ihomPoints_symm_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `LightCondMod` `CommRing.toRing` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryLightCondMod` `CategoryTheory.Functor.obj` `LightCondSet` `CategoryTheory.types` `free` `LightProfinite.toCondensed` `ModuleCat.carrier` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.ihom` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosedLightCondMod` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ihomPoints` `CategoryTheory.CategoryStruct.comp` `lightProfiniteToLightCondSet` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Functor.map` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `Quiver.Hom.op`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `LightProfinite.instPreregular` `CategoryTheory.coherentTopology.subcanonical` `CategoryTheory.MonoidalClosed.curry_natural_left` `CategoryTheory.Functor.map_comp` `CategoryTheory.Adjunction.unit_naturality_assoc` `LightCondSet.hom_naturality_apply` `CategoryTheory.NatTrans.naturality_apply`
`ihom_map_val_app` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `LightCondMod` `instCategoryLightCondensed` `CategoryTheory.ihom` `instMonoidalCategoryLightCondMod` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosedLightCondMod` `Opposite.op` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.map` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `LightCondSet` `CategoryTheory.types` `free` `LightProfinite.toCondensed` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ihomPoints` `CategoryTheory.CategoryStruct.comp`	—	`Equiv.injective` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `LightProfinite.instPreregular` `CategoryTheory.coherentTopology.subcanonical` `Equiv.apply_symm_apply` `hom_ext` `CategoryTheory.types_ext` `CategoryTheory.NatTrans.naturality_apply`
`internallyProjective_iff_tensor_condition` 📖	mathematical	—	`CategoryTheory.InternallyProjective` `LightCondMod` `CommRing.toRing` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryLightCondMod` `instMonoidalClosedLightCondMod` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Functor.comp` `LightCondSet` `CategoryTheory.types` `lightProfiniteToLightCondSet` `free` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Functor.map` `LightProfinite.toCondensed`	—	`CategoryTheory.Functor.PreservesEpimorphisms.preserves` `LightCondMod.epi_iff_locallySurjective_on_lightProfinite` `Equiv.injective` `ihom_map_val_app` `ihomPoints_symm_comp` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply`
`internallyProjective_iff_tensor_condition'` 📖	mathematical	—	`CategoryTheory.InternallyProjective` `LightCondMod` `CommRing.toRing` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryLightCondMod` `instMonoidalClosedLightCondMod` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Functor.comp` `LightCondSet` `CategoryTheory.types` `lightProfiniteToLightCondSet` `free` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Functor.map` `LightProfinite.toCondensed`	—	`internallyProjective_iff_tensor_condition` `CategoryTheory.Category.assoc` `CategoryTheory.BraidedCategory.braiding_naturality_right_assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.BraidedCategory.braiding_inv_naturality_left_assoc` `CategoryTheory.Iso.hom_inv_id_assoc`

---

← Back to Index