Ideal

📁 Source: Mathlib/CategoryTheory/Monoidal/Closed/Ideal.lean

Statistics

Metric	Count
Definitions ofReflective, ExponentialIdeal, bijection, cartesianClosedOfReflective, cartesianClosedOfReflective', exponentialIdealReflective	6
Theorems exp_closed, mk', mk_of_iso, of_exponentialIdeal, bijection_natural, bijection_symm_apply_id, exponentialIdeal_of_preservesBinaryProducts, instExponentialIdealId, instExponentialIdealSubterminalsSubterminalInclusion, preservesBinaryProducts_of_exponentialIdeal, prodComparison_iso, reflective_products	12
Total	18

CategoryTheory

Definitions

Name	Category	Theorems
ExponentialIdeal 📖	CompData	5 math math: ExponentialIdeal.mk', instExponentialIdealSubterminalsSubterminalInclusion, instExponentialIdealId, exponentialIdeal_of_preservesBinaryProducts, ExponentialIdeal.mk_of_iso
bijection 📖	CompOp	2 math math: bijection_natural, bijection_symm_apply_id
cartesianClosedOfReflective 📖	CompOp	—
cartesianClosedOfReflective' 📖	CompOp	—
exponentialIdealReflective 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijection_natural 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Functor.obj reflector MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory EquivLike.toFunLike Equiv.instEquivLike bijection CategoryStruct.comp	—	MonoidalClosed.homEquiv_symm_apply_eq MonoidalClosed.homEquiv_apply_eq Functor.map_injective Reflective.toFaithful Functor.FullyFaithful.map_preimage Functor.map_comp Adjunction.homEquiv_unit Category.comp_id Category.assoc MonoidalClosed.curry_natural_right unitCompPartialBijective_natural MonoidalClosed.uncurry_natural_right
bijection_symm_apply_id 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Functor.obj reflector EquivLike.toFunLike Equiv.instEquivLike Equiv.symm bijection CategoryStruct.id CartesianMonoidalCategory.prodComparison	—	Functor.map_id Category.comp_id unitCompPartialBijective_symm_apply MonoidalClosed.homEquiv_symm_apply_eq MonoidalClosed.homEquiv_apply_eq MonoidalClosed.uncurry_natural_left MonoidalClosed.uncurry_curry BraidedCategory.braiding_naturality_left_assoc SymmetricCategory.symmetry_assoc MonoidalCategory.whisker_exchange_assoc MonoidalCategory.tensorHom_def'_assoc Adjunction.homEquiv_symm_apply Adjunction.eq_unit_comp_map_iff Iso.comp_inv_eq Category.assoc Limits.PreservesLimitsOfShape.preservesLimit Functor.instPreservesLimitsOfShapeOfIsRightAdjoint instIsRightAdjointOfMonadicRightAdjoint CartesianMonoidalCategory.prodComparisonIso_hom CartesianMonoidalCategory.hom_ext CartesianMonoidalCategory.tensorHom_fst CartesianMonoidalCategory.prodComparison_fst Functor.map_comp NatTrans.naturality CartesianMonoidalCategory.tensorHom_snd CartesianMonoidalCategory.prodComparison_snd
exponentialIdeal_of_preservesBinaryProducts 📖	mathematical	—	ExponentialIdeal	—	ExponentialIdeal.mk' CartesianMonoidalCategory.isIso_prodComparison_of_preservesLimit_pair Limits.PreservesLimitsOfShape.preservesLimit MonoidalClosed.curry_natural_left MonoidalClosed.curry_eq_iff MonoidalClosed.uncurry_id_eq_ev Adjunction.homEquiv_naturality_left Adjunction.homEquiv_apply_eq Category.assoc CartesianMonoidalCategory.prodComparison_natural_whiskerLeft_assoc MonoidalCategory.whiskerLeft_comp_assoc Adjunction.left_triangle_components MonoidalCategory.whiskerLeft_id Category.id_comp IsIso.hom_inv_id_assoc mem_essImage_of_unit_isSplitMono IsSplitMono.mk'
instExponentialIdealId 📖	mathematical	—	ExponentialIdeal Functor.id	—	ExponentialIdeal.mk'
instExponentialIdealSubterminalsSubterminalInclusion 📖	mathematical	—	ExponentialIdeal Subterminals instCategorySubterminals subterminalInclusion	—	ExponentialIdeal.mk' MonoidalClosed.uncurry_injective ObjectProperty.FullSubcategory.property
preservesBinaryProducts_of_exponentialIdeal 📖	mathematical	—	Limits.PreservesLimitsOfShape Discrete Limits.WalkingPair discreteCategory reflector	—	Limits.preservesLimit_of_iso_diagram CartesianMonoidalCategory.preservesLimit_pair_of_isIso_prodComparison prodComparison_iso
prodComparison_iso 📖	mathematical	—	IsIso Functor.obj reflector MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CartesianMonoidalCategory.prodComparison	—	Equiv.injective bijection_natural bijection_symm_apply_id Equiv.apply_symm_apply Category.id_comp
reflective_products 📖	mathematical	—	Limits.HasFiniteProducts	—	hasLimitsOfShape_of_reflective Limits.hasLimitsOfShape_discrete Finite.of_fintype

CategoryTheory.CartesianMonoidalCategory

Definitions

Name	Category	Theorems
ofReflective 📖	CompOp	—

CategoryTheory.ExponentialIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp_closed 📖	mathematical	CategoryTheory.Functor.essImage	CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalClosed.closed	—	—
mk' 📖	mathematical	CategoryTheory.Functor.essImage CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalClosed.closed	CategoryTheory.ExponentialIdeal	—	CategoryTheory.Functor.essImage.ofIso
mk_of_iso 📖	mathematical	—	CategoryTheory.ExponentialIdeal	—	mk'

CategoryTheory.Limits.PreservesFiniteProducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_exponentialIdeal 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.reflector	—	CategoryTheory.preservesBinaryProducts_of_exponentialIdeal CategoryTheory.leftAdjoint_preservesTerminal_of_reflective of_preserves_binary_and_terminal CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts

---

← Back to Index