Sections

📁 Source: Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean

Statistics

Metric	Count
Definitions coreHomEquivToOverSections, sections, sectionsCurry, sectionsUncurry, toOverSectionsAdj, curryRightUnitorHom	6
Theorems coreHomEquivToOverSections_homEquiv, sectionsCurry_sectionUncurry, sectionsUncurry_sectionsCurry, sections_map, sections_obj, toOverSectionsAdj_counit_app, toOverSectionsAdj_unit_app, toUnit_comp_curryRightUnitorHom	8
Total	14

CategoryTheory

Definitions

Name	Category	Theorems
curryRightUnitorHom 📖	CompOp	4 math math: Over.toOverSectionsAdj_counit_app, Over.sections_obj, Over.sections_map, toUnit_comp_curryRightUnitorHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toUnit_comp_curryRightUnitorHom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Functor.obj ihom SemiCartesianMonoidalCategory.toUnit curryRightUnitorHom MonoidalClosed.curry SemiCartesianMonoidalCategory.fst	—	MonoidalClosed.uncurry_injective MonoidalClosed.uncurry_natural_left MonoidalClosed.uncurry_curry SemiCartesianMonoidalCategory.fst_def

CategoryTheory.Over

Definitions

Name	Category	Theorems
coreHomEquivToOverSections 📖	CompOp	1 math math: coreHomEquivToOverSections_homEquiv
sections 📖	CompOp	5 math math: toOverSectionsAdj_unit_app, toOverSectionsAdj_counit_app, sections_obj, sections_map, coreHomEquivToOverSections_homEquiv
sectionsCurry 📖	CompOp	4 math math: sectionsUncurry_sectionsCurry, toOverSectionsAdj_unit_app, sectionsCurry_sectionUncurry, coreHomEquivToOverSections_homEquiv
sectionsUncurry 📖	CompOp	4 math math: sectionsUncurry_sectionsCurry, toOverSectionsAdj_counit_app, sectionsCurry_sectionUncurry, coreHomEquivToOverSections_homEquiv
toOverSectionsAdj 📖	CompOp	2 math math: toOverSectionsAdj_unit_app, toOverSectionsAdj_counit_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coreHomEquivToOverSections_homEquiv 📖	mathematical	—	CategoryTheory.Adjunction.CoreHomEquiv.homEquiv CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.toOver sections coreHomEquivToOverSections Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj sectionsCurry sectionsUncurry sectionsUncurry_sectionsCurry sectionsCurry_sectionUncurry	—	—
sectionsCurry_sectionUncurry 📖	mathematical	—	sectionsCurry sectionsUncurry	—	CategoryTheory.SymmetricCategory.symmetry_assoc CategoryTheory.MonoidalClosed.curry_uncurry CategoryTheory.ChosenPullbacksAlong.lift.congr_simp CategoryTheory.ChosenPullbacksAlong.hom_ext CategoryTheory.ChosenPullbacksAlong.lift_fst CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
sectionsUncurry_sectionsCurry 📖	mathematical	—	sectionsUncurry sectionsCurry	—	OverMorphism.ext homMk.congr_simp CategoryTheory.ChosenPullbacksAlong.lift_fst CategoryTheory.MonoidalClosed.uncurry_curry CategoryTheory.SymmetricCategory.symmetry_assoc
sections_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.instCategoryOver sections CategoryTheory.ChosenPullbacksAlong.pullbackMap CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.curryRightUnitorHom CategoryTheory.CommaMorphism.left CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
sections_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver sections CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.ihom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.curryRightUnitorHom	—	—
toOverSectionsAdj_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp sections CategoryTheory.toOver CategoryTheory.Functor.id CategoryTheory.Adjunction.counit toOverSectionsAdj sectionsUncurry CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.curryRightUnitorHom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toOverSectionsAdj_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.toOver sections CategoryTheory.Adjunction.unit toOverSectionsAdj sectionsCurry CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

---

← Back to Index