End

📁 Source: Mathlib/CategoryTheory/Monoidal/End.lean

Statistics

Metric	Count
Definitions End, End, End, instMonoidalFunctorTensoringRight, endofunctorMonoidalCategory, equivOfTensorIsoUnit, unitOfTensorIsoUnit, End, End, End, End, End, End	13
Theorems tensoringRight_δ, tensoringRight_ε, tensoringRight_η, tensoringRight_μ, associativity_app, associativity_app_assoc, endofunctorMonoidalCategory_associator_hom_app, endofunctorMonoidalCategory_associator_inv_app, endofunctorMonoidalCategory_leftUnitor_hom_app, endofunctorMonoidalCategory_leftUnitor_inv_app, endofunctorMonoidalCategory_rightUnitor_hom_app, endofunctorMonoidalCategory_rightUnitor_inv_app, endofunctorMonoidalCategory_tensorMap_app, endofunctorMonoidalCategory_tensorObj_map, endofunctorMonoidalCategory_tensorObj_obj, endofunctorMonoidalCategory_tensorUnit_map, endofunctorMonoidalCategory_tensorUnit_obj, endofunctorMonoidalCategory_whiskerLeft_app, endofunctorMonoidalCategory_whiskerRight_app, equivOfTensorIsoUnit_counitIso, equivOfTensorIsoUnit_functor, equivOfTensorIsoUnit_inverse, equivOfTensorIsoUnit_unitIso, left_unitality_app, left_unitality_app_assoc, obj_zero_map_μ_app, obj_zero_map_μ_app_assoc, obj_ε_app, obj_ε_app_assoc, obj_η_app, obj_η_app_assoc, obj_μ_app, obj_μ_app_assoc, obj_μ_inv_app, obj_μ_inv_app_assoc, obj_μ_zero_app, right_unitality_app, right_unitality_app_assoc, unitOfTensorIsoUnit_hom_app, unitOfTensorIsoUnit_inv_app, δ_naturality, δ_naturality_assoc, δ_naturalityᵣ, δ_naturalityᵣ_assoc, δ_naturalityₗ, δ_naturalityₗ_assoc, δ_μ_app, δ_μ_app_assoc, ε_app_obj, ε_naturality, ε_naturality_assoc, ε_η_app, ε_η_app_assoc, η_app_obj, η_naturality, η_naturality_assoc, η_ε_app, η_ε_app_assoc, μ_naturality, μ_naturality_assoc, μ_naturalityᵣ, μ_naturalityᵣ_assoc, μ_naturality₂, μ_naturality₂_assoc, μ_naturalityₗ, μ_naturalityₗ_assoc, μ_δ_app, μ_δ_app_assoc	68
Total	81

AddMonoid

Definitions

Name	Category	Theorems
End 📖	CompOp	62 math math: CentroidHom.toEnd_pow, End.natCast_apply, CentroidHom.toEnd_sub, CentroidHom.toEnd_one, WithLp.prod_norm_eq_idemFst_of_L1, End.ofNat_apply, End.mulRight_apply_apply, AddMonoidAlgebra.divOfHom_apply_apply, commute_lmul_rmul, WithLp.idemSnd_compl, CentroidHom.centroid_eq_centralizer_mulLeftRight, DistribMulAction.toAddMonoidEnd_apply, two_nsmul_lie_lmul_lmul_add_add_eq_zero, CentroidHom.toEnd_smul, End.instAddMonoidHomClass, CentroidHom.toEnd_add, End.intCast_apply, commute_lmul_sq_rmul, End.smul_apply, CentroidHom.toEnd_intCast, monoidEndToAdditive_apply_apply, WithLp.prod_norm_eq_idemFst_sup_idemSnd, commute_lmul_rmul_sq, End.mulLeft_apply_apply, End.smul_def, WithLp.prod_norm_eq_add_idemFst, WithLp.idemFst_compl, MulEquiv.AddMonoid.End_apply, NonUnitalNonAssocCommSemiring.mem_center_iff, End.coe_mul, addMonoidEndRingEquivInt_apply, commute_lmul_lmul_sq, End.isCentralScalar, two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add, End.coe_pow, End.natCast_def, End.coe_one, monoidEndToAdditive_symm_apply_apply, CentroidHom.toEnd_natCast, CentroidHom.toEnd_zero, End.smulCommClass, End.applyFaithfulSMul, CentroidHom.toEndRingHom_apply, WithLp.idemSnd_apply, CentroidHom.toEnd_injective, CentroidHom.toEnd_mul, NonUnitalNonAssocSemiring.mem_center_iff, WithLp.idemFst_add_idemSnd, WithLp.idemFst_apply, End.intCast_def, CentroidHom.toEnd_neg, End.isScalarTower, Module.toAddMonoidEnd_apply_apply, End.one_apply, End.coe_smul, MulEquiv.Monoid.End_apply, addMonoidEndRingEquivInt_symm_apply, addMonoidEndToMultiplicative_apply_apply, AddSubgroup.pointwise_smul_def, commute_rmul_rmul_sq, addMonoidEndToMultiplicative_symm_apply_apply, End.zero_apply

AlgHom

Definitions

Name	Category	Theorems
End 📖	CompOp	23 math math: ContinuousAlgHom.toAlgHomMonoidHom_apply, coe_galRestrict_apply, mul_apply, one_apply, galRestrictHom_symm_algebraMap_apply, AlgEquiv.algHomUnitsEquiv_apply_symm_apply, AlgEquiv.val_algHomUnitsEquiv_symm_apply, Algebra.smul_units_def, galRestrict_apply, AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply, Algebra.IsAlgebraic.algEquivEquivAlgHom_apply, End_toOne_one, galRestrictHom_symm_apply, FiniteField.bijective_frobeniusAlgHom_pow, Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply, toEnd_apply, AlgEquiv.toAlgHomHom_apply, FiniteField.orderOf_frobeniusAlgHom, galRestrictHom_apply, algebraMap_galRestrictHom_apply, AlgEquiv.algHomUnitsEquiv_apply_apply, End_toSemigroup_toMul_mul, coe_pow

BialgHom

Definitions

Name	Category	Theorems
End 📖	CompOp	4 math math: End_toSemigroup_toMul_mul, End_toOne_one, mul_apply, one_apply

CategoryTheory

Definitions

Name	Category	Theorems
endofunctorMonoidalCategory 📖	CompOp	103 math math: Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app, endofunctorMonoidalCategory_tensorUnit_obj, obj_ε_app_assoc, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom, Monad.ofMon_η, MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomLeft, Monad.mul_def, δ_naturalityₗ_assoc, η_naturality_assoc, endofunctorMonoidalCategory_tensorObj_obj, μ_δ_app_assoc, η_ε_app_assoc, Monad.monadMonEquiv_counitIso_hom_app_hom, μ_naturality₂_assoc, MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso, ε_η_app_assoc, ε_naturality_assoc, Monad.monadToMon_obj, obj_zero_map_μ_app_assoc, μ_naturalityᵣ_assoc, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app, MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv, MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_η_app, MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom, obj_μ_app, μ_naturalityₗ, δ_naturalityᵣ_assoc, MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv, Monad.monToMonad_obj, left_unitality_app_assoc, μ_naturality₂, μ_naturalityᵣ, endofunctorMonoidalCategory_associator_inv_app, δ_μ_app, MonoidalCategory.tensoringRight_δ, endofunctorMonoidalCategory_whiskerRight_app, right_unitality_app_assoc, η_app_obj, MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomRight, endofunctorMonoidalCategory_tensorMap_app, Monad.monadToMon_map_hom, μ_naturality, obj_zero_map_μ_app, Monad.toMon_mon, endofunctorMonoidalCategory_tensorObj_map, endofunctorMonoidalCategory_rightUnitor_inv_app, η_naturality, ε_naturality, MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_ε_app, endofunctorMonoidalCategory_whiskerLeft_app, unitOfTensorIsoUnit_inv_app, obj_η_app_assoc, MonoidalCategory.tensoringRight_ε, Monad.monToMonad_map_toNatTrans, ε_app_obj, obj_μ_inv_app, associativity_app_assoc, endofunctorMonoidalCategory_leftUnitor_hom_app, MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_μ_app, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app, Monad.monadMonEquiv_inverse, endofunctorMonoidalCategory_associator_hom_app, μ_δ_app, left_unitality_app, MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionObj, ε_η_app, δ_naturality_assoc, Monad.ofMon_μ, δ_naturality, MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_δ_app, MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso, Monad.monadMonEquiv_counitIso_inv_app_hom, obj_μ_app_assoc, endofunctorMonoidalCategory_rightUnitor_hom_app, Monad.ofMon_obj, endofunctorMonoidalCategory_tensorUnit_map, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv, obj_μ_zero_app, Monad.monadMonEquiv_functor, endofunctorMonoidalCategory_leftUnitor_inv_app, associativity_app, obj_μ_inv_app_assoc, δ_naturalityₗ, Monad.toMon_X, μ_naturality_assoc, δ_naturalityᵣ, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv, unitOfTensorIsoUnit_hom_app, Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app, obj_ε_app, MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom, δ_μ_app_assoc, Monad.one_def, obj_η_app, right_unitality_app, η_ε_app, μ_naturalityₗ_assoc, MonoidalCategory.tensoringRight_η, isMonoidalLeftDistrib.of_endofunctors, MonoidalCategory.tensoringRight_μ
equivOfTensorIsoUnit 📖	CompOp	4 math math: equivOfTensorIsoUnit_unitIso, equivOfTensorIsoUnit_counitIso, equivOfTensorIsoUnit_functor, equivOfTensorIsoUnit_inverse
unitOfTensorIsoUnit 📖	CompOp	4 math math: equivOfTensorIsoUnit_unitIso, equivOfTensorIsoUnit_counitIso, unitOfTensorIsoUnit_inv_app, unitOfTensorIsoUnit_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associativity_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.map NatTrans.app Functor.LaxMonoidal.μ Iso.hom MonoidalCategoryStruct.associator	—	congr_app Functor.LaxMonoidal.associativity Category.id_comp
associativity_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.map NatTrans.app Functor.LaxMonoidal.μ Iso.hom MonoidalCategoryStruct.associator	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associativity_app
endofunctorMonoidalCategory_associator_hom_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Iso.hom MonoidalCategoryStruct.associator CategoryStruct.id Category.toCategoryStruct Functor.obj	—	—
endofunctorMonoidalCategory_associator_inv_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Iso.inv MonoidalCategoryStruct.associator CategoryStruct.id Category.toCategoryStruct Functor.obj	—	—
endofunctorMonoidalCategory_leftUnitor_hom_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.leftUnitor CategoryStruct.id Category.toCategoryStruct Functor.obj	—	—
endofunctorMonoidalCategory_leftUnitor_inv_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.leftUnitor CategoryStruct.id Category.toCategoryStruct Functor.obj	—	—
endofunctorMonoidalCategory_rightUnitor_hom_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.rightUnitor CategoryStruct.id Category.toCategoryStruct Functor.obj	—	—
endofunctorMonoidalCategory_rightUnitor_inv_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.rightUnitor CategoryStruct.id Category.toCategoryStruct Functor.obj	—	—
endofunctorMonoidalCategory_tensorMap_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory MonoidalCategoryStruct.tensorHom CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.map	—	—
endofunctorMonoidalCategory_tensorObj_map 📖	mathematical	—	Functor.map MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.obj	—	—
endofunctorMonoidalCategory_tensorObj_obj 📖	mathematical	—	Functor.obj MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory	—	—
endofunctorMonoidalCategory_tensorUnit_map 📖	mathematical	—	Functor.map MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory	—	—
endofunctorMonoidalCategory_tensorUnit_obj 📖	mathematical	—	Functor.obj MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory	—	—
endofunctorMonoidalCategory_whiskerLeft_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory MonoidalCategoryStruct.whiskerLeft Functor.obj	—	—
endofunctorMonoidalCategory_whiskerRight_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory MonoidalCategoryStruct.whiskerRight Functor.map Functor.obj	—	—
equivOfTensorIsoUnit_counitIso 📖	mathematical	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.whiskerRight Iso.hom MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerLeft MonoidalCategoryStruct.rightUnitor	Equivalence.counitIso equivOfTensorIsoUnit unitOfTensorIsoUnit	—	—
equivOfTensorIsoUnit_functor 📖	mathematical	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.whiskerRight Iso.hom MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerLeft MonoidalCategoryStruct.rightUnitor	Equivalence.functor equivOfTensorIsoUnit Functor.obj Functor Functor.category	—	—
equivOfTensorIsoUnit_inverse 📖	mathematical	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.whiskerRight Iso.hom MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerLeft MonoidalCategoryStruct.rightUnitor	Equivalence.inverse equivOfTensorIsoUnit Functor.obj Functor Functor.category	—	—
equivOfTensorIsoUnit_unitIso 📖	mathematical	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.whiskerRight Iso.hom MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerLeft MonoidalCategoryStruct.rightUnitor	Equivalence.unitIso equivOfTensorIsoUnit Iso.symm Functor Functor.category Functor.comp Functor.obj Functor.id unitOfTensorIsoUnit	—	—
left_unitality_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.map NatTrans.app Functor.LaxMonoidal.ε MonoidalCategoryStruct.tensorObj Functor.LaxMonoidal.μ Iso.hom MonoidalCategoryStruct.leftUnitor CategoryStruct.id	—	congr_app Functor.LaxMonoidal.left_unitality
left_unitality_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.map NatTrans.app Functor.LaxMonoidal.ε MonoidalCategoryStruct.tensorObj Functor.LaxMonoidal.μ Iso.hom MonoidalCategoryStruct.leftUnitor	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' left_unitality_app
obj_zero_map_μ_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorObj Functor.map NatTrans.app endofunctorMonoidalCategory Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal Iso.inv MonoidalCategoryStruct.rightUnitor	—	cancel_epi IsSplitEpi.epi IsSplitEpi.of_iso NatIso.isIso_app_of_isIso Functor.Monoidal.instIsIsoε cancel_mono IsSplitMono.mono IsSplitMono.of_iso Functor.Monoidal.instIsIsoδ ε_naturality_assoc ε_app_obj Category.assoc δ_μ_app Category.comp_id ε_η_app_assoc
obj_zero_map_μ_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct Functor.map MonoidalCategoryStruct.tensorObj NatTrans.app endofunctorMonoidalCategory Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal Iso.inv MonoidalCategoryStruct.rightUnitor	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' obj_zero_map_μ_app
obj_ε_app 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.ε Functor.Monoidal.toLaxMonoidal CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Iso.inv MonoidalCategoryStruct.leftUnitor Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal	—	Functor.Monoidal.map_leftUnitor_inv Category.id_comp Category.assoc μ_δ_app Category.comp_id
obj_ε_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.map NatTrans.app Functor.LaxMonoidal.ε Functor.Monoidal.toLaxMonoidal MonoidalCategoryStruct.tensorObj Iso.inv MonoidalCategoryStruct.leftUnitor Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' obj_ε_app
obj_η_app 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Iso.hom MonoidalCategoryStruct.leftUnitor	—	cancel_mono IsSplitMono.mono instIsSplitMonoMap IsSplitMono.of_iso NatIso.isIso_app_of_isIso Functor.Monoidal.instIsIsoε Functor.map_comp η_ε_app Functor.map_id obj_ε_app Category.assoc Iso.map_hom_inv_id_app_assoc μ_δ_app
obj_η_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.map NatTrans.app Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal MonoidalCategoryStruct.tensorObj Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Iso.hom MonoidalCategoryStruct.leftUnitor	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' obj_η_app
obj_μ_app 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal CategoryStruct.comp Category.toCategoryStruct Iso.inv MonoidalCategoryStruct.associator Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal	—	associativity_app_assoc Iso.map_hom_inv_id_app_assoc μ_δ_app Category.comp_id
obj_μ_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.map NatTrans.app Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Iso.inv MonoidalCategoryStruct.associator Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' obj_μ_app
obj_μ_inv_app 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal CategoryStruct.comp Category.toCategoryStruct Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Iso.hom MonoidalCategoryStruct.associator	—	Functor.Monoidal.map_associator Category.id_comp Category.assoc μ_δ_app_assoc μ_δ_app Category.comp_id
obj_μ_inv_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.map NatTrans.app Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Iso.hom MonoidalCategoryStruct.associator	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' obj_μ_inv_app
obj_μ_zero_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory MonoidalCategoryStruct.tensorUnit NatTrans.app Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Functor.map Iso.inv MonoidalCategoryStruct.associator Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal Iso.hom MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.rightUnitor	—	obj_η_app_assoc Functor.map_comp η_app_obj Category.assoc Iso.map_hom_inv_id_app Category.comp_id obj_μ_app
right_unitality_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.ε Functor.Monoidal.toLaxMonoidal MonoidalCategoryStruct.tensorObj Functor.LaxMonoidal.μ Functor.map Iso.hom MonoidalCategoryStruct.rightUnitor CategoryStruct.id	—	congr_app Functor.LaxMonoidal.right_unitality
right_unitality_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.ε Functor.Monoidal.toLaxMonoidal MonoidalCategoryStruct.tensorObj Functor.LaxMonoidal.μ Functor.map Iso.hom MonoidalCategoryStruct.rightUnitor	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' right_unitality_app
unitOfTensorIsoUnit_hom_app 📖	mathematical	—	NatTrans.app Functor.comp Functor.obj Functor Functor.category Functor.id Iso.hom unitOfTensorIsoUnit CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Functor.LaxMonoidal.μ endofunctorMonoidalCategory Functor.Monoidal.toLaxMonoidal MonoidalCategoryStruct.tensorUnit Functor.map Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal	—	—
unitOfTensorIsoUnit_inv_app 📖	mathematical	—	NatTrans.app Functor.id Functor.comp Functor.obj Functor Functor.category Iso.inv unitOfTensorIsoUnit CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct Functor.LaxMonoidal.ε endofunctorMonoidalCategory Functor.Monoidal.toLaxMonoidal MonoidalCategoryStruct.tensorObj Functor.map Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal	—	Category.assoc
δ_naturality 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.δ Functor.map	—	NatTrans.naturality
δ_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.δ Functor.map	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_naturality
δ_naturalityᵣ 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.δ Functor.map MonoidalCategoryStruct.whiskerLeft	—	congr_app Functor.OplaxMonoidal.δ_natural_right
δ_naturalityᵣ_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.δ Functor.map MonoidalCategoryStruct.whiskerLeft	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_naturalityᵣ
δ_naturalityₗ 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.δ Functor.map MonoidalCategoryStruct.whiskerRight	—	congr_app Functor.OplaxMonoidal.δ_natural_left
δ_naturalityₗ_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.δ Functor.map MonoidalCategoryStruct.whiskerRight	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_naturalityₗ
δ_μ_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal CategoryStruct.id	—	Iso.inv_hom_id_app
δ_μ_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_μ_app
ε_app_obj 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.obj Functor.LaxMonoidal.ε Functor.Monoidal.toLaxMonoidal CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Functor.map Iso.inv MonoidalCategoryStruct.rightUnitor Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal	—	Functor.Monoidal.map_rightUnitor_inv Category.id_comp Category.assoc μ_δ_app Category.comp_id
ε_naturality 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.ε Functor.map	—	NatTrans.naturality
ε_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.ε Functor.map	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ε_naturality
ε_η_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.ε Functor.Monoidal.toLaxMonoidal Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal CategoryStruct.id	—	Iso.hom_inv_id_app
ε_η_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.ε Functor.Monoidal.toLaxMonoidal Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ε_η_app
η_app_obj 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Functor.map Iso.hom MonoidalCategoryStruct.rightUnitor	—	Functor.Monoidal.map_rightUnitor Category.comp_id μ_δ_app_assoc
η_naturality 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.η Functor.map	—	—
η_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.η Functor.map	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' η_naturality
η_ε_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal Functor.LaxMonoidal.ε Functor.Monoidal.toLaxMonoidal CategoryStruct.id	—	Iso.inv_hom_id_app
η_ε_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.OplaxMonoidal.η Functor.Monoidal.toOplaxMonoidal Functor.LaxMonoidal.ε Functor.Monoidal.toLaxMonoidal	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' η_ε_app
μ_naturality 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Functor.map NatTrans.app endofunctorMonoidalCategory Functor.LaxMonoidal.μ	—	NatTrans.naturality
μ_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category Functor.map MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct NatTrans.app endofunctorMonoidalCategory Functor.LaxMonoidal.μ	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_naturality
μ_naturalityᵣ 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct NatTrans.app Functor.map endofunctorMonoidalCategory Functor.LaxMonoidal.μ MonoidalCategoryStruct.whiskerLeft	—	MonoidalCategory.id_tensorHom μ_naturality₂ Functor.map_id Category.id_comp
μ_naturalityᵣ_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category NatTrans.app Functor.map MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.LaxMonoidal.μ MonoidalCategoryStruct.whiskerLeft	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_naturalityᵣ
μ_naturality₂ 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct NatTrans.app Functor.map endofunctorMonoidalCategory Functor.LaxMonoidal.μ MonoidalCategoryStruct.tensorHom	—	congr_app Functor.LaxMonoidal.μ_natural Category.assoc
μ_naturality₂_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category NatTrans.app Functor.map MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.LaxMonoidal.μ MonoidalCategoryStruct.tensorHom	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_naturality₂
μ_naturalityₗ 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Functor.map NatTrans.app endofunctorMonoidalCategory Functor.LaxMonoidal.μ MonoidalCategoryStruct.whiskerRight	—	MonoidalCategory.tensorHom_id μ_naturality₂ Functor.map_id Category.id_comp
μ_naturalityₗ_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor Functor.category Functor.map NatTrans.app MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory Functor.LaxMonoidal.μ MonoidalCategoryStruct.whiskerRight	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_naturalityₗ
μ_δ_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal CategoryStruct.id	—	Iso.hom_inv_id_app
μ_δ_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct endofunctorMonoidalCategory NatTrans.app Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' μ_δ_app

CategoryTheory.MonoidalCategory

Definitions

Name	Category	Theorems
instMonoidalFunctorTensoringRight 📖	CompOp	4 math math: tensoringRight_δ, tensoringRight_ε, tensoringRight_η, tensoringRight_μ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensoringRight_δ 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category tensoringRight CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalFunctorTensoringRight CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	—
tensoringRight_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory tensoringRight CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalFunctorTensoringRight CategoryTheory.Iso.inv tensorUnitRight CategoryTheory.Functor.id rightUnitorNatIso	—	—
tensoringRight_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory tensoringRight CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalFunctorTensoringRight CategoryTheory.Iso.hom tensorUnitRight CategoryTheory.Functor.id rightUnitorNatIso	—	—
tensoringRight_μ 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category toMonoidalCategoryStruct CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Functor.obj tensoringRight CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalFunctorTensoringRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	—

CoalgHom

Definitions

Name	Category	Theorems
End 📖	CompOp	4 math math: mul_apply, End_toOne_one, one_apply, End_toSemigroup_toMul_mul

Function

Definitions

Name	Category	Theorems
End 📖	CompOp	16 math math: End.mul_def, Equiv.Perm.val_equivUnitsEnd_apply, MonoidHom.toHomPerm_apply_symm_apply, AddConstMap.toEnd_apply, LipschitzWith.mul_end, LipschitzWith.pow_end, LipschitzWith.list_prod, LocallyLipschitz.pow_end, End.smul_def, LocallyLipschitz.mul_end, Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply, Equiv.Perm.equivUnitsEnd_symm_apply_apply, MonoidHom.toHomPerm_apply_apply, End.one_def, Equiv.Perm.val_inv_equivUnitsEnd_apply, End.apply_FaithfulSMul

Monoid

Definitions

Name	Category	Theorems
End 📖	CompOp	12 math math: End.coe_one, End.coe_pow, Subgroup.pointwise_smul_def, monoidEndToAdditive_apply_apply, MulEquiv.AddMonoid.End_apply, End.coe_mul, monoidEndToAdditive_symm_apply_apply, MulEquiv.Monoid.End_apply, addMonoidEndToMultiplicative_apply_apply, MulDistribMulAction.toMonoidEnd_apply, End.instMonoidHomClass, addMonoidEndToMultiplicative_symm_apply_apply

MulEquiv.AddMonoid

Definitions

Name	Category	Theorems
End 📖	CompOp	1 math math: End_apply

MulEquiv.Monoid

Definitions

Name	Category	Theorems
End 📖	CompOp	1 math math: End_apply

RootPairing

Definitions

Name	Category	Theorems
End 📖	CompOp	6 math math: Equiv.weightHom_toLinearMap, Equiv.toEndUnit_inv, Hom.coweightHom_injective, Equiv.coweightHom_toLinearMap, Hom.weightHom_injective, Equiv.toEndUnit_val

---

← Back to Index