Monoidal

📁 Source: Mathlib/CategoryTheory/Sites/Point/Monoidal.lean

Statistics

Metric	Count
Definitions instMonoidalFunctorOppositePresheafFiber, instMonoidalSheafSheafFiber, instOplaxMonoidalFunctorOppositePresheafFiber	3
Theorems instIsIsoδFunctorOppositePresheafFiber, instIsIsoηFunctorOppositePresheafFiber, instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso, instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor, instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor, tensorHom_comp_toPresheafFiber_μ, tensorHom_comp_toPresheafFiber_μ_assoc, toPresheafFiber_δ, toPresheafFiber_δ_assoc, toPresheafFiber_ε, toPresheafFiber_η, toPresheafFiber_η_assoc	12
Total	15

CategoryTheory.GrothendieckTopology.Point

Definitions

Name	Category	Theorems
instMonoidalFunctorOppositePresheafFiber 📖	CompOp	4 math math: tensorHom_comp_toPresheafFiber_μ_assoc, tensorHom_comp_toPresheafFiber_μ, instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso, toPresheafFiber_ε
instMonoidalSheafSheafFiber 📖	CompOp	1 math math: instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso
instOplaxMonoidalFunctorOppositePresheafFiber 📖	CompOp	6 math math: instIsIsoδFunctorOppositePresheafFiber, toPresheafFiber_δ_assoc, toPresheafFiber_δ, toPresheafFiber_η, instIsIsoηFunctorOppositePresheafFiber, toPresheafFiber_η_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoδFunctorOppositePresheafFiber 📖	mathematical	CategoryTheory.Limits.PreservesFilteredColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.OplaxMonoidal.δ instOplaxMonoidalFunctorOppositePresheafFiber	—	CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.PreservesColimit₂.of_preservesColimits_in_each_variable CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor instIsSiftedOppositeElementsFiber
instIsIsoηFunctorOppositePresheafFiber 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.OplaxMonoidal.η instOplaxMonoidalFunctorOppositePresheafFiber	—	CategoryTheory.Iso.isIso_hom CategoryTheory.IsFiltered.isConnected CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered
instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso 📖	mathematical	CategoryTheory.Limits.PreservesFilteredColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.IsMonoidal CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.comp CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.presheafToSheaf sheafFiber presheafFiber CategoryTheory.Iso.hom presheafToSheafCompSheafFiberIso CategoryTheory.Functor.LaxMonoidal.comp CategoryTheory.Sheaf.monoidalCategory CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Sheaf.instMonoidalFunctorOppositePresheafToSheaf instMonoidalSheafSheafFiber instMonoidalFunctorOppositePresheafFiber	—	CategoryTheory.Localization.Monoidal.lifting_isMonoidal CategoryTheory.GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities CategoryTheory.ObjectProperty.instIsMultiplicativeIsLocal
instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor 📖	mathematical	CategoryTheory.Limits.PreservesFilteredColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.Limits.PreservesColimitsOfShape Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor	—	CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered CategoryTheory.instLocallySmallOpposite CategoryTheory.CategoryOfElements.instLocallySmallElements CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel
instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor 📖	mathematical	CategoryTheory.Limits.PreservesFilteredColimitsOfSize CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Limits.PreservesColimitsOfShape Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.curriedTensor	—	CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered CategoryTheory.instLocallySmallOpposite CategoryTheory.CategoryOfElements.instLocallySmallElements CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel
tensorHom_comp_toPresheafFiber_μ 📖	mathematical	CategoryTheory.Limits.PreservesFilteredColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom toPresheafFiber CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalFunctorOppositePresheafFiber CategoryTheory.Monoidal.functorCategoryMonoidalStruct	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso instIsIsoδFunctorOppositePresheafFiber CategoryTheory.Category.assoc CategoryTheory.Functor.Monoidal.μ_δ CategoryTheory.Category.comp_id toPresheafFiber_δ
tensorHom_comp_toPresheafFiber_μ_assoc 📖	mathematical	CategoryTheory.Limits.PreservesFilteredColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.MonoidalCategoryStruct.tensorHom toPresheafFiber CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalFunctorOppositePresheafFiber CategoryTheory.Monoidal.functorCategoryMonoidalStruct	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorHom_comp_toPresheafFiber_μ
toPresheafFiber_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidalStruct Opposite.op presheafFiber CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toPresheafFiber CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Monoidal.functorCategoryMonoidal instOplaxMonoidalFunctorOppositePresheafFiber CategoryTheory.MonoidalCategoryStruct.tensorHom	—	toPresheafFiber_presheafFiberDesc
toPresheafFiber_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidalStruct Opposite.op presheafFiber toPresheafFiber CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Monoidal.functorCategoryMonoidal instOplaxMonoidalFunctorOppositePresheafFiber CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_δ
toPresheafFiber_ε 📖	mathematical	CategoryTheory.Limits.PreservesFilteredColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidal presheafFiber CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalFunctorOppositePresheafFiber toPresheafFiber CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Monoidal.functorCategoryMonoidalStruct	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso instIsIsoηFunctorOppositePresheafFiber CategoryTheory.Functor.Monoidal.ε_η toPresheafFiber_η
toPresheafFiber_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidalStruct Opposite.op presheafFiber CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toPresheafFiber CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Monoidal.functorCategoryMonoidal instOplaxMonoidalFunctorOppositePresheafFiber CategoryTheory.CategoryStruct.id	—	toPresheafFiber_presheafFiberDesc
toPresheafFiber_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidalStruct Opposite.op presheafFiber toPresheafFiber CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Monoidal.functorCategoryMonoidal instOplaxMonoidalFunctorOppositePresheafFiber CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_η

---

← Back to Index