Basic

📁 Source: Mathlib/CategoryTheory/Center/Basic.lean

Statistics

Metric	Count
Definitions CatCenter, app, instSMulHom, instSMulUnitsIso	4
Theorems ext, ext_iff, instIsMulCommutative, mul_app, mul_app', mul_app'_assoc, mul_app_assoc, naturality, naturality_assoc, smul_eq, smul_eq', smul_iso_hom_eq, smul_iso_hom_eq', smul_iso_hom_eq'_assoc, smul_iso_hom_eq_assoc, smul_iso_inv_eq, smul_iso_inv_eq', smul_iso_inv_eq'_assoc, smul_iso_inv_eq_assoc	19
Total	23

CategoryTheory

Definitions

Name	Category	Theorems
CatCenter 📖	CompOp	42 math math: TwistShiftData.z_zero_zero, CatCenter.app_sub, Linear.smulOfRingMorphism_smul_eq', Functor.commShift₂_comm, CatCenter.smul_iso_inv_eq', CatCenter.mul_app, CatCenter.smul_iso_inv_eq'_assoc, CatCenter.mul_app', TwistShiftData.assoc, Linear.smulOfRingMorphism_smul_eq, CatCenter.app_add, TwistShiftData.shift_z_app, CatCenter.smul_iso_hom_eq'_assoc, CatCenter.mul_app_assoc, CatCenter.smul_eq', Functor.CommShift₂.comm, TwistShiftData.z_zero_left, CatCenter.smul_iso_inv_eq_assoc, CatCenter.smul_eq, CatCenter.mul_app'_assoc, CatCenter.smul_iso_hom_eq_assoc, CatCenter.smul_iso_inv_eq, CatCenter.app_neg_one_zpow, CatCenter.localization_zero, TwistShiftData.shiftFunctorAdd'_inv_app, CatCenter.smul_iso_hom_eq', TwistShiftData.shiftFunctorAdd'_hom_app, CatCenter.localization_mul, CatCenter.instIsMulCommutative, TwistShiftData.commShift, CatCenter.localization_one, Linear.toCatCenter_apply_app, CatCenter.app_neg, CatCenter.smul_iso_hom_eq, CommShift₂Setup.z_zero₂, CommShift₂Setup.int_ε, Functor.commShift₂_comm_assoc, CommShift₂Setup.z_zero₁, CommShift₂Setup.hε, CatCenter.localization_add, CommShift₂Setup.int_z, TwistShiftData.z_zero_right

CategoryTheory.CatCenter

Definitions

Name	Category	Theorems
app 📖	CompOp	28 math math: ext_iff, app_sub, localization_app, naturality_assoc, CategoryTheory.Linear.smulOfRingMorphism_smul_eq', CategoryTheory.Functor.commShift₂_comm, smul_iso_inv_eq', mul_app, smul_iso_inv_eq'_assoc, naturality, mul_app', CategoryTheory.Linear.smulOfRingMorphism_smul_eq, app_add, CategoryTheory.TwistShiftData.shift_z_app, smul_iso_hom_eq'_assoc, mul_app_assoc, smul_eq', CategoryTheory.Functor.CommShift₂.comm, smul_iso_inv_eq_assoc, smul_eq, mul_app'_assoc, smul_iso_hom_eq_assoc, smul_iso_inv_eq, app_neg_one_zpow, smul_iso_hom_eq', app_neg, smul_iso_hom_eq, CategoryTheory.Functor.commShift₂_comm_assoc
instSMulHom 📖	CompOp	4 math math: smul_eq', smul_eq, CategoryTheory.TwistShiftData.shiftFunctorAdd'_inv_app, CategoryTheory.TwistShiftData.shiftFunctorAdd'_hom_app
instSMulUnitsIso 📖	CompOp	8 math math: smul_iso_inv_eq', smul_iso_inv_eq'_assoc, smul_iso_hom_eq'_assoc, smul_iso_inv_eq_assoc, smul_iso_hom_eq_assoc, smul_iso_inv_eq, smul_iso_hom_eq', smul_iso_hom_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	app	—	—	CategoryTheory.NatTrans.ext
ext_iff 📖	mathematical	—	app	—	ext
instIsMulCommutative 📖	mathematical	—	IsMulCommutative CategoryTheory.CatCenter CategoryTheory.End.mul CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id	—	ext mul_app' mul_app
mul_app 📖	mathematical	—	app CategoryTheory.CatCenter CategoryTheory.End.mul CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp	—	mul_app' naturality
mul_app' 📖	mathematical	—	app CategoryTheory.CatCenter CategoryTheory.End.mul CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp	—	—
mul_app'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct app CategoryTheory.CatCenter CategoryTheory.End.mul CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_app'
mul_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct app CategoryTheory.CatCenter CategoryTheory.End.mul CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_app
naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct app	—	CategoryTheory.NatTrans.naturality
naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality
smul_eq 📖	mathematical	—	CategoryTheory.CatCenter Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instSMulHom CategoryTheory.CategoryStruct.comp app	—	—
smul_eq' 📖	mathematical	—	CategoryTheory.CatCenter Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instSMulHom CategoryTheory.CategoryStruct.comp app	—	naturality
smul_iso_hom_eq 📖	mathematical	—	CategoryTheory.Iso.hom Units CategoryTheory.CatCenter CategoryTheory.End.monoid CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Iso instSMulUnitsIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct app Units.val	—	—
smul_iso_hom_eq' 📖	mathematical	—	CategoryTheory.Iso.hom Units CategoryTheory.CatCenter CategoryTheory.End.monoid CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Iso instSMulUnitsIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct app Units.val	—	naturality
smul_iso_hom_eq'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom Units CategoryTheory.CatCenter CategoryTheory.End.monoid CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Iso instSMulUnitsIso app Units.val	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' smul_iso_hom_eq'
smul_iso_hom_eq_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom Units CategoryTheory.CatCenter CategoryTheory.End.monoid CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Iso instSMulUnitsIso app Units.val	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' smul_iso_hom_eq
smul_iso_inv_eq 📖	mathematical	—	CategoryTheory.Iso.inv Units CategoryTheory.CatCenter CategoryTheory.End.monoid CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Iso instSMulUnitsIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct app Units.val Units.instInv	—	—
smul_iso_inv_eq' 📖	mathematical	—	CategoryTheory.Iso.inv Units CategoryTheory.CatCenter CategoryTheory.End.monoid CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Iso instSMulUnitsIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct app Units.val Units.instInv	—	naturality
smul_iso_inv_eq'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv Units CategoryTheory.CatCenter CategoryTheory.End.monoid CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Iso instSMulUnitsIso app Units.val Units.instInv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' smul_iso_inv_eq'
smul_iso_inv_eq_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv Units CategoryTheory.CatCenter CategoryTheory.End.monoid CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Iso instSMulUnitsIso app Units.val Units.instInv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' smul_iso_inv_eq

---

← Back to Index