| Metric | Count |
|---|
Definitionsmap, obj, map, obj, app', arrow, arrowEquiv, hom, homMk, homMkSucc, homMkā, homMkā, homMkā, homMkā, homMkā, homMkā
, isoMk, isoMkSucc, isoMkā, isoMkā, isoMkā, isoMkā, isoMkā, isoMkā
, left, map', mkOfObjOfMapSucc, mkā, mkā, mkā, mkā, mkā, mkā
, obj', opEquivalence, precomp, right, tacticValid, whiskerLeft, whiskerLeftFunctor, Ī“last, Ī“lastFunctor, Ī“ā, Ī“āFunctor, mapComposableArrows, mapComposableArrowsObjMkāIso, mapComposableArrowsObjMkāIso, mapComposableArrowsOpIso, castSuccFunctor, succFunctor | 50 |
Theoremsmap_comp, map_id, map_comp, map_id, map_one_one, map_one_succ, map_succ_succ, map_zero_one, map_zero_one', map_zero_succ_succ, map_zero_zero, obj_one, obj_succ, obj_zero, arrowEquiv_apply, arrowEquiv_symm_apply, ext, ext_succ, extā, extā, extā, extā_of_arrow, extā, extā, extā
, homMkSucc_app_succ, homMkSucc_app_zero, homMk_app, homMkā_app, homMkā_app, homMkā_app_one, homMkā_app_two, homMkā_app_two', homMkā_app_zero, homMkā_app_one, homMkā_app_three, homMkā_app_two, homMkā_app_zero, homMkā_app_four, homMkā_app_one, homMkā_app_three, homMkā_app_two, homMkā_app_zero, homMkā
_app_five, homMkā
_app_four, homMkā
_app_one, homMkā
_app_three, homMkā
_app_two, homMkā
_app_zero, hom_ext_succ, hom_extā, hom_extā_iff, hom_extā, hom_extā_iff, hom_extā, hom_extā_iff, hom_extā, hom_extā_iff, hom_extā, hom_extā_iff, hom_extā
, hom_extā
_iff, isIso_iffā, isIso_iffā, isIso_iffā, isoMkSucc_hom, isoMkSucc_inv, isoMk_hom, isoMk_inv, isoMkā_hom_app, isoMkā_inv_app, isoMkā_hom_app, isoMkā_inv_app, isoMkā_hom, isoMkā_inv, isoMkā_hom, isoMkā_inv, isoMkā_hom, isoMkā_inv, isoMkā
_hom, isoMkā
_inv, map'_comp, map'_eq_homā, map'_inv_eq_inv_map', map'_self, mkOfObjOfMapSucc_arrow, mkOfObjOfMapSucc_exists, mkOfObjOfMapSucc_map_succ, mkOfObjOfMapSucc_obj, mkā_map, mkā_obj, mkā_surjective, mkā_comp_eqToHom, mkā_eqToHom_comp, mkā_hom, mkā_map, mkā_obj, mkā_surjective, mkā_surjective, mkā_surjective, mkā_surjective, mkā
_surjective, naturality', naturality'_assoc, opEquivalence_counitIso_hom_app_app, opEquivalence_counitIso_inv_app_app, opEquivalence_functor_map_app, opEquivalence_functor_obj_map, opEquivalence_functor_obj_obj, opEquivalence_inverse_map, opEquivalence_inverse_obj, opEquivalence_unitIso_hom_app, opEquivalence_unitIso_inv_app, precomp_map, precomp_obj, precomp_surjective, precomp_Ī“ā, whiskerLeftFunctor_map_app, whiskerLeftFunctor_obj_map, whiskerLeftFunctor_obj_obj, whiskerLeft_map, whiskerLeft_obj, Ī“lastFunctor_map_app, Ī“lastFunctor_obj_map, Ī“lastFunctor_obj_obj, Ī“āFunctor_map_app, Ī“āFunctor_obj_map, Ī“āFunctor_obj_obj, mapComposableArrowsObjMkāIso_hom_app, mapComposableArrowsObjMkāIso_inv_app, mapComposableArrowsObjMkāIso_hom_app, mapComposableArrowsObjMkāIso_inv_app, mapComposableArrows_map_app, mapComposableArrows_obj_map, mapComposableArrows_obj_obj, castSuccFunctor_map, castSuccFunctor_obj, succFunctor_map, succFunctor_obj | 139 |
| Total | 189 |
| Name | Category | Theorems |
|---|
app' š | CompOp | 19 mathmath: hom_extā
_iff, CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono', CategoryTheory.Abelian.mono_of_epi_of_epi_mono', CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono', CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono', CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono, CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono, CategoryTheory.Abelian.epi_of_epi_of_epi_of_epi, hom_extā_iff, CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono, naturality', CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono, hom_extā_iff, hom_extā_iff, hom_extā_iff, hom_extā_iff, naturality'_assoc, CategoryTheory.Abelian.mono_of_epi_of_epi_of_mono, CategoryTheory.Abelian.mono_of_mono_of_mono_of_mono
|
arrow š | CompOp | 1 mathmath: mkOfObjOfMapSucc_arrow
|
arrowEquiv š | CompOp | 2 mathmath: arrowEquiv_symm_apply, arrowEquiv_apply
|
hom š | CompOp | 15 mathmath: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, mkā_hom, CategoryTheory.nerve.homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.nerve.mkā_homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, map'_eq_homā, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, arrowEquiv_apply, SSet.OneTruncationā.nerveHomEquiv_apply, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom
|
homMk š | CompOp | 3 mathmath: isoMk_inv, isoMk_hom, homMk_app
|
homMkSucc š | CompOp | 4 mathmath: isoMkSucc_hom, homMkSucc_app_zero, isoMkSucc_inv, homMkSucc_app_succ
|
homMkā š | CompOp | 1 mathmath: homMkā_app
|
homMkā š | CompOp | 8 mathmath: CategoryTheory.Triangulated.SpectralObject.Ļā_map_homā, mapFunctorArrows_app, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_morā, CategoryTheory.Triangulated.SpectralObject.Ļā_map_homā, functorArrows_map, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_morā, CategoryTheory.Triangulated.SpectralObject.Ļā_map_homā, homMkā_app
|
homMkā š | CompOp | 6 mathmath: homMkā_app_two, isoMkā_inv, homMkā_app_zero, isoMkā_hom, homMkā_app_one, homMkā_app_two'
|
homMkā š | CompOp | 7 mathmath: homMkā_app_three, isoMkā_hom, homMkā_app_two, isoMkā_inv, homMkā_app_one, HomologicalComplex.HomologySequence.composableArrowsāFunctor_map, homMkā_app_zero
|
homMkā š | CompOp | 7 mathmath: homMkā_app_four, homMkā_app_three, homMkā_app_zero, isoMkā_hom, homMkā_app_one, isoMkā_inv, homMkā_app_two
|
homMkā
š | CompOp | 9 mathmath: homMkā
_app_five, homMkā
_app_zero, isoMkā
_inv, CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map, homMkā
_app_two, homMkā
_app_three, isoMkā
_hom, homMkā
_app_one, homMkā
_app_four
|
isoMk š | CompOp | 2 mathmath: isoMk_inv, isoMk_hom
|
isoMkSucc š | CompOp | 2 mathmath: isoMkSucc_hom, isoMkSucc_inv
|
isoMkā š | CompOp | 2 mathmath: isoMkā_inv_app, isoMkā_hom_app
|
isoMkā š | CompOp | 2 mathmath: isoMkā_hom_app, isoMkā_inv_app
|
isoMkā š | CompOp | 2 mathmath: isoMkā_inv, isoMkā_hom
|
isoMkā š | CompOp | 2 mathmath: isoMkā_hom, isoMkā_inv
|
isoMkā š | CompOp | 2 mathmath: isoMkā_hom, isoMkā_inv
|
isoMkā
š | CompOp | 2 mathmath: isoMkā
_inv, isoMkā
_hom
|
left š | CompOp | 16 mathmath: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, mkā_hom, CategoryTheory.nerve.homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, Precomp.map_zero_succ_succ, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.nerve.left_edge, CategoryTheory.nerve.mkā_homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, arrowEquiv_apply, SSet.OneTruncationā.nerveHomEquiv_apply, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom
|
map' š | CompOp | 49 mathmath: HomotopyCategory.spectralObjectMappingCone_Ī“'_app, exact_iff_Ī“last, Exact.cokerIsoKer'_hom_inv_id_assoc, IsComplex.zero'_assoc, CategoryTheory.nerve.Ī“ā_zero, CategoryTheory.instMonoMap'KernelCokernelCompSequenceOfNatNat, Exact.cokerIsoKer'_hom, IsComplex.opcyclesToCycles_fac_assoc, Precomp.map_zero_succ_succ, HomologicalComplex.HomologySequence.instEpiMap'ComposableArrowsāOfNatNat, exact_iff_Ī“ā, mkOfObjOfMapSucc_map_succ, IsComplex.mono_cokerToKer', map'_comp, IsComplex.zero_assoc, Exact.opcyclesIsoCycles_hom_fac_assoc, Exact.opcyclesIsoCycles_hom_fac, IsComplex.opcyclesToCycles_fac, Exact.cokerIsoKer'_inv_hom_id, HomotopyCategory.composableArrowsFunctor_obj, mapFunctorArrows_app, Exact.cokerIsoKer'_hom_inv_id, naturality', CategoryTheory.instEpiMap'KernelCokernelCompSequenceOfNatNat, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_morā, isComplexā_iff, Exact.cokerIsoKer'_inv_hom_id_assoc, HomotopyCategory.composableArrowsFunctor_map, Exact.cokerIsoKer_hom_fac_assoc, map'_eq_homā, HomologicalComplex.HomologySequence.instMonoMap'ComposableArrowsāOfNatNat, Exact.cokerIsoKer_hom_fac, IsComplex.epi_cokerToKer', map'_self, Exact.isIso_cokerToKer', Precomp.map_succ_succ, mkOfObjOfMapSucc_exists, functorArrows_map, IsComplex.cokerToKer'_fac_assoc, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_morā, naturality'_assoc, Precomp.map_one_succ, functorArrows_obj, IsComplex.cokerToKer'_fac, IsComplex.zero, IsComplex.cokerToKer_fac, CategoryTheory.nerve.Ī“ā_two, IsComplex.zero', IsComplex.cokerToKer_fac_assoc
|
mkOfObjOfMapSucc š | CompOp | 3 mathmath: mkOfObjOfMapSucc_arrow, mkOfObjOfMapSucc_map_succ, mkOfObjOfMapSucc_obj
|
mkā š | CompOp | 5 mathmath: mkā_surjective, mkā_obj, CategoryTheory.nerve.Ļā_mkā_eq, mkā_map, CategoryTheory.nerveMap_app_mkā
|
mkā š | CompOp | 51 mathmath: CategoryTheory.Triangulated.SpectralObject.Hom.comm, CategoryTheory.nerve.edgeMk_edge, CategoryTheory.Functor.mapComposableArrowsObjMkāIso_inv_app, CategoryTheory.nerve.Ī“ā_zero, twoĪ“āToĪ“ā_app_zero, CategoryTheory.Functor.mapComposableArrowsObjMkāIso_inv_app, mkā_eqToHom_comp, mkā_hom, mkā_surjective, mkOfObjOfMapSucc_arrow, CategoryTheory.Triangulated.SpectralObject.Ļā_map_homā, twoĪ“āToĪ“ā_app_zero, CategoryTheory.Triangulated.SpectralObject.triangle_objā, CategoryTheory.nerve.mkā_homEquiv_apply, mkā_comp_eqToHom, CategoryTheory.nerveMap_app_mkā, CategoryTheory.Functor.mapComposableArrowsObjMkāIso_hom_app, arrowEquiv_symm_apply, mkā_obj, CategoryTheory.Functor.mapComposableArrowsObjMkāIso_hom_app, CategoryTheory.Triangulated.SpectralObject.triangle_morā, CategoryTheory.nerve.Ī“ā_mkā_eq, CategoryTheory.Triangulated.SpectralObject.Hom.comm_assoc, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_morā, twoĪ“āToĪ“ā_app_one, mkā_map, SSet.Truncated.HomotopyCategory.homToNerveMk_app_one, CategoryTheory.nerve.Ļā_mkā_eq, CategoryTheory.Triangulated.SpectralObject.triangle_morā, CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_Ī“, CategoryTheory.nerve.Ī“ā_mkā_eq, instIsIsoOfNatNatTwoĪ“āToĪ“ā, CategoryTheory.ShortComplex.toComposableArrows_map, CategoryTheory.nerve.Ļ_zero_nerveEquiv_symm, twoĪ“āToĪ“ā_app_one, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, CategoryTheory.ShortComplex.toComposableArrows_obj, CategoryTheory.Triangulated.SpectralObject.Ļā_map_homā, CategoryTheory.Triangulated.SpectralObject.triangle_objā, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_objā, CategoryTheory.Triangulated.SpectralObject.triangle_objā, functorArrows_map, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_morā, CategoryTheory.Triangulated.SpectralObject.Ļā_map_homā, instIsIsoOfNatNatTwoĪ“āToĪ“ā, functorArrows_obj, CategoryTheory.nerve.Ī“ā_mkā_eq, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_objā, CategoryTheory.nerve.Ī“ā_two, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_objā, CategoryTheory.nerve.homEquiv_symm_apply
|
mkā š | CompOp | 19 mathmath: threeĪ“āToĪ“ā_app_zero, CategoryTheory.Functor.mapComposableArrowsObjMkāIso_inv_app, exact_iff_Ī“last, threeĪ“āToĪ“ā_app_one, threeĪ“āToĪ“ā_app_zero, threeĪ“āToĪ“ā_app_one, threeĪ“āToĪ“ā_app_two, exact_iff_Ī“ā, CochainComplex.mappingConeCompTriangle_morā_naturality, CategoryTheory.Functor.mapComposableArrowsObjMkāIso_hom_app, CategoryTheory.nerve.Ī“ā_mkā_eq, threeĪ“āToĪ“ā_app_two, CategoryTheory.nerve.Ī“ā_mkā_eq, threeĪ“āToĪ“ā_app_two, threeĪ“āToĪ“ā_app_one, threeĪ“āToĪ“ā_app_zero, CochainComplex.mappingConeCompTriangle_morā_naturality_assoc, CategoryTheory.nerve.Ī“ā_mkā_eq, mkā_surjective
|
mkā š | CompOp | 17 mathmath: fourĪ“āToĪ“ā_app_zero, fourĪ“āToĪ“ā_app_two, fourĪ“āToĪ“ā_app_one, fourĪ“āToĪ“ā_app_three, fourĪ“āToĪ“ā_app_zero, fourĪ“āToĪ“ā_app_two, fourĪ“āToĪ“ā_app_one, fourĪ“āToĪ“ā_app_one, mkā_surjective, fourĪ“āToĪ“ā_app_two, fourĪ“āToĪ“ā_app_two, fourĪ“āToĪ“ā_app_three, fourĪ“āToĪ“ā_app_one, fourĪ“āToĪ“ā_app_zero, fourĪ“āToĪ“ā_app_three, fourĪ“āToĪ“ā_app_three, fourĪ“āToĪ“ā_app_zero
|
mkā š | CompOp | 1 mathmath: mkā_surjective
|
mkā
š | CompOp | 1 mathmath: mkā
_surjective
|
obj' š | CompOp | 17 mathmath: CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono', CategoryTheory.Abelian.mono_of_epi_of_epi_mono', CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono', CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono', Precomp.obj_one, CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono, CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono, CategoryTheory.Abelian.epi_of_epi_of_epi_of_epi, CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono, naturality', CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_morā, Precomp.obj_succ, CategoryTheory.Triangulated.SpectralObject.Ļā_obj_morā, naturality'_assoc, CategoryTheory.Abelian.mono_of_epi_of_epi_of_mono, CategoryTheory.Abelian.mono_of_mono_of_mono_of_mono
|
opEquivalence š | CompOp | 9 mathmath: opEquivalence_counitIso_inv_app_app, opEquivalence_unitIso_inv_app, opEquivalence_functor_obj_map, opEquivalence_functor_map_app, opEquivalence_inverse_obj, opEquivalence_unitIso_hom_app, opEquivalence_functor_obj_obj, opEquivalence_inverse_map, opEquivalence_counitIso_hom_app_app
|
precomp š | CompOp | 4 mathmath: precomp_obj, precomp_Ī“ā, precomp_surjective, precomp_map
|
right š | CompOp | 15 mathmath: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, mkā_hom, CategoryTheory.nerve.homEquiv_apply, CategoryTheory.nerve.right_edge, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.nerve.mkā_homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, arrowEquiv_apply, SSet.OneTruncationā.nerveHomEquiv_apply, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom
|
tacticValid š | CompOp | ā |
whiskerLeft š | CompOp | 3 mathmath: whiskerLeft_obj, whiskerLeft_map, CategoryTheory.nerve_map
|
whiskerLeftFunctor š | CompOp | 3 mathmath: whiskerLeftFunctor_obj_map, whiskerLeftFunctor_obj_obj, whiskerLeftFunctor_map_app
|
Ī“last š | CompOp | 2 mathmath: exact_iff_Ī“last, Exact.Ī“last
|
Ī“lastFunctor š | CompOp | 3 mathmath: Ī“lastFunctor_obj_obj, Ī“lastFunctor_map_app, Ī“lastFunctor_obj_map
|
Ī“ā š | CompOp | 4 mathmath: exact_iff_Ī“ā, precomp_Ī“ā, CategoryTheory.nerve.Ī“ā_eq, Exact.Ī“ā
|
Ī“āFunctor š | CompOp | 3 mathmath: Ī“āFunctor_obj_map, Ī“āFunctor_obj_obj, Ī“āFunctor_map_app
|