Monoidal

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

Statistics

Metric	Count
Definitions instMonoidalCategoryLightCondMod, instMonoidalCategorySheafLightProfiniteCoherentTopologyModuleCat, instMonoidalClosedFunctorOppositeLightProfiniteModuleCat, instMonoidalClosedLightCondMod, instMonoidalClosedSheafLightProfiniteCoherentTopologyModuleCat, instMonoidalFunctorOppositeLightProfiniteModuleCatSheafCoherentTopologyPresheafToSheaf, instMonoidalLightCondSetLightCondModFree, instSymmetricCategoryLightCondMod	8
Theorems instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology	1
Total	9

LightCondensed

Definitions

Name	Category	Theorems
instMonoidalCategoryLightCondMod 📖	CompOp	10 math math: free_internallyProjective_iff_tensor_condition, ihomPoints_apply, ihomPoints_symm_comp, free_lightProfinite_internallyProjective_iff_tensor_condition, internallyProjective_iff_tensor_condition, free_lightProfinite_internallyProjective_iff_tensor_condition', free_internallyProjective_iff_tensor_condition', ihomPoints_symm_apply, ihom_map_val_app, internallyProjective_iff_tensor_condition'
instMonoidalCategorySheafLightProfiniteCoherentTopologyModuleCat 📖	CompOp	—
instMonoidalClosedFunctorOppositeLightProfiniteModuleCat 📖	CompOp	—
instMonoidalClosedLightCondMod 📖	CompOp	10 math math: free_internallyProjective_iff_tensor_condition, ihomPoints_apply, ihomPoints_symm_comp, free_lightProfinite_internallyProjective_iff_tensor_condition, internallyProjective_iff_tensor_condition, free_lightProfinite_internallyProjective_iff_tensor_condition', free_internallyProjective_iff_tensor_condition', ihomPoints_symm_apply, ihom_map_val_app, internallyProjective_iff_tensor_condition'
instMonoidalClosedSheafLightProfiniteCoherentTopologyModuleCat 📖	CompOp	—
instMonoidalFunctorOppositeLightProfiniteModuleCatSheafCoherentTopologyPresheafToSheaf 📖	CompOp	—
instMonoidalLightCondSetLightCondModFree 📖	CompOp	—
instSymmetricCategoryLightCondMod 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMonoidal CategoryTheory.Functor Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.W CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular CategoryTheory.Monoidal.functorCategoryMonoidal ModuleCat.monoidalCategory	—	CategoryTheory.GrothendieckTopology.W.transport_isMonoidal CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular instEssentiallySmallLightProfinite CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Equivalence.full_inverse CategoryTheory.coherentTopology.instIsCoverDense CategoryTheory.Functor.instEffectivelyEnoughOfIsEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Equivalence.faithful_inverse CategoryTheory.Functor.IsDenseSubsite.instIsContinuous CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense CategoryTheory.Functor.IsEquivalence.essSurj CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits ModuleCat.hasLimits' CategoryTheory.GrothendieckTopology.W.monoidal ModuleCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self

---

← Back to Index