CatCommSq

📁 Source: Mathlib/CategoryTheory/CatCommSq.lean

Statistics

Metric	Count
Definitions CatCommSq, hComp, hComp', hId, hInv, hInvEquiv, iso, vComp, vComp', vId, vInv, vInvEquiv	12
Theorems ext, ext_iff, hComp_iso_hom_app, hComp_iso_inv_app, hId_iso_hom_app, hId_iso_inv_app, hInv_hInv, hInv_iso_hom_app, hInv_iso_inv_app, iso_hom_naturality, iso_hom_naturality_assoc, iso_inv_naturality, iso_inv_naturality_assoc, vComp_iso_hom_app, vComp_iso_inv_app, vId_iso_hom_app, vId_iso_inv_app, vInv_iso_hom_app, vInv_iso_inv_app, vInv_vInv	20
Total	32

CategoryTheory

Definitions

Name	Category	Theorems
CatCommSq 📖	CompData	2 math math: Limits.CatCospanTransform.id_squareLeft, Limits.CatCospanTransform.id_squareRight

CategoryTheory.CatCommSq

Definitions

Name	Category	Theorems
hComp 📖	CompOp	2 math math: hComp_iso_hom_app, hComp_iso_inv_app
hComp' 📖	CompOp	—
hId 📖	CompOp	2 math math: hId_iso_hom_app, hId_iso_inv_app
hInv 📖	CompOp	3 math math: hInv_iso_inv_app, hInv_hInv, hInv_iso_hom_app
hInvEquiv 📖	CompOp	—
iso 📖	CompOp	65 math math: CategoryTheory.Limits.CategoricalPullback.catCommSq_iso_hom_app, CategoryTheory.Adjunction.Localization.ε_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_app_snd_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_snd_app, hInv_iso_inv_app, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_app_assoc, hId_iso_hom_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.asSquare_iso, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_inv_app_snd_app, hComp_iso_hom_app, iso_inv_naturality, CategoryTheory.Adjunction.localization_unit_app, CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_app_assoc, vId_iso_hom_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_app_fst_app, hId_iso_inv_app, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_map_fst_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_fst_app, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac, vInv_iso_hom_app, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_map_snd_app, iso_hom_naturality, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_app, vComp_iso_hom_app, iso_inv_naturality_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_id, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_inv_app_snd_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_comp, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_snd_app, CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence, CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_app, CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_map_fst_app, vInv_iso_inv_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_naturality₂, CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_app_assoc, hComp_iso_inv_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_inv_app_fst_app, CategoryTheory.Adjunction.localization_counit_app, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.guitartExact', CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_id, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_app_snd_app, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_app, vComp_iso_inv_app, CategoryTheory.Limits.CategoricalPullback.catCommSq_iso_inv_app, CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_assoc, CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_naturality₂, iso_hom_naturality_assoc, ext_iff, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformPrecomposeObjSquare_iso_hom_comp, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_iso_inv_app, CategoryTheory.LocalizerMorphism.instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_app_fst_app, hInv_iso_hom_app, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_fst_app, vId_iso_inv_app, CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_map_snd_app, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence, CategoryTheory.Adjunction.Localization.η_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_inv_app_fst_app, CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.guitartExact', CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_iso_hom_app
vComp 📖	CompOp	2 math math: vComp_iso_hom_app, vComp_iso_inv_app
vComp' 📖	CompOp	2 math math: CategoryTheory.Limits.CatCospanTransform.comp_squareRight, CategoryTheory.Limits.CatCospanTransform.comp_squareLeft
vId 📖	CompOp	4 math math: vId_iso_hom_app, CategoryTheory.Limits.CatCospanTransform.id_squareLeft, CategoryTheory.Limits.CatCospanTransform.id_squareRight, vId_iso_inv_app
vInv 📖	CompOp	3 math math: vInv_iso_hom_app, vInv_iso_inv_app, vInv_vInv
vInvEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	iso	—	—	—
ext_iff 📖	mathematical	—	iso	—	ext
hComp_iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso hComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
hComp_iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso hComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
hId_iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso hId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Category.comp_id
hId_iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso hId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Category.comp_id
hInv_hInv 📖	mathematical	—	hInv CategoryTheory.Equivalence.symm	—	ext CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' CategoryTheory.cancel_mono CategoryTheory.IsIso.mono_of_iso CategoryTheory.Functor.map_isIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Functor.comp_map CategoryTheory.NatTrans.naturality hInv_iso_hom_app hInv_iso_inv_app CategoryTheory.Equivalence.counitInv_app_functor CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp CategoryTheory.Equivalence.fun_inv_map CategoryTheory.Equivalence.counitInv_functor_comp CategoryTheory.Iso.inv_hom_id_app_assoc
hInv_iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso hInv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc
hInv_iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso hInv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Equivalence.counitIso CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
iso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso	—	CategoryTheory.NatTrans.naturality
iso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_hom_naturality
iso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso	—	CategoryTheory.NatTrans.naturality
iso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_inv_naturality
vComp_iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso vComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
vComp_iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso vComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
vId_iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso vId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Category.comp_id
vId_iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso vId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Category.comp_id
vInv_iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso vInv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id CategoryTheory.Category.assoc
vInv_iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso vInv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp
vInv_vInv 📖	mathematical	—	vInv CategoryTheory.Equivalence.symm	—	ext CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' vInv_iso_hom_app vInv_iso_inv_app CategoryTheory.cancel_mono CategoryTheory.IsIso.mono_of_iso CategoryTheory.Functor.map_isIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Functor.comp_map CategoryTheory.Functor.map_comp CategoryTheory.Equivalence.fun_inv_map CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.Equivalence.counit_app_functor CategoryTheory.NatTrans.comp_app CategoryTheory.Iso.inv_hom_id CategoryTheory.NatTrans.id_app CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.hom_inv_id iso_hom_naturality

---

← Back to Index