| Metric | Count |
|---|
DefinitionsisoHomologyι₀, isoHomologyπ₀, ExactAt, HasHomology, cycles, cyclesFunctor, cyclesIsKernel, cyclesIsoSc', cyclesMap, cyclesMapIso, descOpcycles, descOpcycles', fromOpcycles, gradedHomologyFunctor, homology, homologyFunctor, homologyFunctorIso, homologyFunctorIso', homologyIsCokernel, homologyIsKernel, homologyIsoSc', homologyMap, homologyMapIso, homologyι, homologyπ, iCycles, iCyclesIso, isoHomologyι, isoHomologyπ, isoSc', liftCycles, liftCycles', natIsoSc', natTransHomologyι, natTransHomologyπ, opcycles, opcyclesFunctor, opcyclesIsCokernel, opcyclesIsoSc', opcyclesMap, opcyclesMapIso, pOpcycles, pOpcyclesIso, sc, sc', shortComplexFunctor, shortComplexFunctor', toCycles | 48 |
TheoremsisIso_descOpcycles_iff, isIso_homologyι₀, isoHomologyι₀_inv_naturality, isoHomologyι₀_inv_naturality_assoc, isIso_homologyπ₀, isIso_liftCycles_iff, isoHomologyπ₀_inv_naturality, isoHomologyπ₀_inv_naturality_assoc, isZero_homology, of_iso, acyclic_iff, acyclic_of_isZero, comp_liftCycles, comp_liftCycles_assoc, cyclesFunctor_map, cyclesFunctor_obj, cyclesIsoSc'_hom_iCycles, cyclesIsoSc'_hom_iCycles_assoc, cyclesIsoSc'_inv_iCycles, cyclesIsoSc'_inv_iCycles_assoc, cyclesMapIso_hom, cyclesMapIso_inv, cyclesMap_comp, cyclesMap_comp_assoc, cyclesMap_i, cyclesMap_i_assoc, cyclesMap_id, cyclesMap_zero, d_pOpcycles, d_pOpcycles_assoc, d_toCycles, d_toCycles_assoc, descOpcycles_comp, descOpcycles_comp_assoc, epi_homologyMap_of_epi_of_not_rel, exactAt_iff, exactAt_iff', exactAt_iff_isZero_homology, fromOpcycles_d, fromOpcycles_d_assoc, fromOpcycles_eq_zero, gradedHomologyFunctor_map, gradedHomologyFunctor_obj, hasHomology_of_iso, homologyFunctorIso_hom_app, homologyFunctorIso_inv_app, homologyFunctor_map, homologyFunctor_obj, homologyIsoSc'_hom_ι, homologyIsoSc'_hom_ι_assoc, homologyIsoSc'_inv_ι, homologyIsoSc'_inv_ι_assoc, homologyMapIso_hom, homologyMapIso_inv, homologyMap_add, homologyMap_comp, homologyMap_comp_assoc, homologyMap_id, homologyMap_neg, homologyMap_sub, homologyMap_zero, homology_π_ι, homology_π_ι_assoc, homologyι_comp_fromOpcycles, homologyι_comp_fromOpcycles_assoc, homologyι_descOpcycles_eq_zero_of_boundary, homologyι_descOpcycles_eq_zero_of_boundary_assoc, homologyι_naturality, homologyι_naturality_assoc, homologyπ_naturality, homologyπ_naturality_assoc, iCyclesIso_hom, iCyclesIso_hom_inv_id, iCyclesIso_hom_inv_id_assoc, iCyclesIso_inv_hom_id, iCyclesIso_inv_hom_id_assoc, iCycles_d, iCycles_d_assoc, instAdditiveHomologyFunctor, instEpiHomologyπ, instEpiOpcyclesMapOfF, instEpiPOpcycles, instMonoCyclesMapOfF, instMonoHomologyι, instMonoICycles, instPreservesZeroMorphismsCyclesFunctor, instPreservesZeroMorphismsHomologyFunctor, instPreservesZeroMorphismsOpcyclesFunctor, isIso_homologyι, isIso_homologyπ, isIso_iCycles, isIso_pOpcycles, isoHomologyι_hom, isoHomologyι_hom_inv_id, isoHomologyι_hom_inv_id_assoc, isoHomologyι_inv_hom_id, isoHomologyι_inv_hom_id_assoc, isoHomologyπ_hom, isoHomologyπ_hom_inv_id, isoHomologyπ_hom_inv_id_assoc, isoHomologyπ_inv_hom_id, isoHomologyπ_inv_hom_id_assoc, liftCycles_comp_cyclesMap, liftCycles_comp_cyclesMap_assoc, liftCycles_homologyπ_eq_zero_of_boundary, liftCycles_homologyπ_eq_zero_of_boundary_assoc, liftCycles_i, liftCycles_i_assoc, mono_homologyMap_of_mono_of_not_rel, natIsoSc'_hom_app_τ₁, natIsoSc'_hom_app_τ₂, natIsoSc'_hom_app_τ₃, natIsoSc'_inv_app_τ₁, natIsoSc'_inv_app_τ₂, natIsoSc'_inv_app_τ₃, natTransHomologyι_app, natTransHomologyπ_app, opcyclesFunctor_map, opcyclesFunctor_obj, opcyclesIsoSc'_inv_fromOpcycles, opcyclesIsoSc'_inv_fromOpcycles_assoc, opcyclesMapIso_hom, opcyclesMapIso_inv, opcyclesMap_comp, opcyclesMap_comp_assoc, opcyclesMap_comp_descOpcycles, opcyclesMap_comp_descOpcycles_assoc, opcyclesMap_id, opcyclesMap_zero, pOpcyclesIso_hom, pOpcyclesIso_hom_inv_id, pOpcyclesIso_hom_inv_id_assoc, pOpcyclesIso_inv_hom_id, pOpcyclesIso_inv_hom_id_assoc, pOpcycles_opcyclesIsoSc'_hom, pOpcycles_opcyclesIsoSc'_hom_assoc, pOpcycles_opcyclesIsoSc'_inv, pOpcycles_opcyclesIsoSc'_inv_assoc, p_descOpcycles, p_descOpcycles_assoc, p_fromOpcycles, p_fromOpcycles_assoc, p_opcyclesMap, p_opcyclesMap_assoc, shortComplexFunctor'_map_τ₁, shortComplexFunctor'_map_τ₂, shortComplexFunctor'_map_τ₃, shortComplexFunctor'_obj_X₁, shortComplexFunctor'_obj_X₂, shortComplexFunctor'_obj_X₃, shortComplexFunctor'_obj_f, shortComplexFunctor'_obj_g, shortComplexFunctor_map_τ₁, shortComplexFunctor_map_τ₂, shortComplexFunctor_map_τ₃, shortComplexFunctor_obj_X₁, shortComplexFunctor_obj_X₂, shortComplexFunctor_obj_X₃, shortComplexFunctor_obj_f, shortComplexFunctor_obj_g, toCycles_comp_homologyπ, toCycles_comp_homologyπ_assoc, toCycles_cyclesIsoSc'_hom, toCycles_cyclesIsoSc'_hom_assoc, toCycles_eq_zero, toCycles_i, toCycles_i_assoc, π_homologyIsoSc'_hom, π_homologyIsoSc'_hom_assoc, π_homologyIsoSc'_inv, π_homologyIsoSc'_inv_assoc | 171 |
| Total | 219 |
| Name | Category | Theorems |
|---|
ExactAt 📖 | MathDef | 27 mathmath: exactAt_iff_isZero_homology, extend_exactAt, AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace, extend_exactAt_iff, CategoryTheory.Abelian.LeftResolution.exactAt_map_chainComplex_succ, ChainComplex.exactAt_succ_single_obj, CochainComplex.exactAt_succ_single_obj, exactAt_iff, exactAt_of_isSupported, CochainComplex.exactAt_of_isLE, exactAt_op_iff, IsSupportedOutside.exactAt, CochainComplex.isLE_iff, CochainComplex.exactAt_of_isGE, CochainComplex.isGE_iff, exactAt_iff_of_quasiIsoAt, CategoryTheory.InjectiveResolution.cocomplex_exactAt_succ, ChainComplex.alternatingConst_exactAt, exactAt_single_obj, IsSupported.exactAt, acyclic_iff, CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ, CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt, isSupported_iff, exactAt_iff', CategoryTheory.ProjectiveResolution.complex_exactAt_succ
|
HasHomology 📖 | MathDef | 12 mathmath: restriction.hasHomology, instHasHomologyOppositeOp, instHasHomologyObjSingle, extend.hasHomology, instHasHomologyOppositeObjSymmOpFunctorOp, hasHomology_of_iso, CategoryTheory.ProjectiveResolution.hasHomology, instHasHomologyUnopOfOpposite, ChainComplex.instHasHomologyNatObjAlternatingConst, extend.instHasHomologyF, CategoryTheory.InjectiveResolution.hasHomology, instHasHomologyObjOppositeSymmUnopFunctorOp
|
cycles 📖 | CompOp | 141 mathmath: π_homologyIsoSc'_hom, homologyπ_extendHomologyIso_hom, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, alternatingConst_iCycles_odd_comp_assoc, pOpcycles_opcyclesToCycles_iCycles_assoc, liftCycles_comp_cyclesMap, homologyπ_restrictionHomologyIso_inv_assoc, singleObjCyclesSelfIso_inv_iCycles, toCycles_i, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc, CochainComplex.isoHomologyπ₀_inv_naturality_assoc, opcyclesOpIso_inv_naturality_assoc, instMonoICycles, cyclesMap_comp_assoc, eq_liftCycles_homologyπ_up_to_refinements, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, singleObjCyclesSelfIso_inv_homologyπ, restrictionCyclesIso_hom_iCycles, truncLE'_d_eq_toCycles, d_toCycles_assoc, cyclesMap_id, opcyclesOpIso_inv_naturality, CategoryTheory.instIsIsoToRightDerivedZero', homologyπ_extendHomologyIso_inv, homologyπ_restrictionHomologyIso_inv, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, iCyclesIso_inv_hom_id, comp_liftCycles, cyclesOpIso_inv_naturality_assoc, extendCyclesIso_inv_iCycles_assoc, singleObjCyclesSelfIso_hom_naturality, singleObjCyclesSelfIso_inv_naturality_assoc, homologyι_opcyclesToCycles_assoc, cyclesOpNatIso_inv_app, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, cyclesIsoSc'_inv_iCycles_assoc, CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self, cyclesMap_comp, opcyclesToCycles_iCycles_assoc, homologyπ_singleObjHomologySelfIso_hom_assoc, opcyclesToCycles_naturality, iCycles_d, CochainComplex.isoHomologyπ₀_inv_naturality, isIso_homologyπ, opcyclesOpIso_hom_naturality_assoc, opcyclesToCycles_homologyπ, cyclesIsoSc'_hom_iCycles_assoc, homologyπ_naturality, homologyπ_naturality_assoc, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, opcyclesOpIso_hom_toCycles_op, extendCyclesIso_hom_naturality_assoc, alternatingConst_iCycles_even_comp_apply, d_toCycles, cyclesIsoSc'_inv_iCycles, truncLE'Map_f_eq_cyclesMap, instEpiHomologyπ, instMonoCyclesMapOfF, liftCycles_homologyπ_eq_zero_of_boundary, cyclesMap_i_assoc, singleObjCyclesSelfIso_inv_homologyπ_assoc, fromOpcycles_op_cyclesOpIso_inv_assoc, homologyπ_restrictionHomologyIso_hom, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality, liftCycles_i_assoc, i_cyclesMk, cyclesOpIso_inv_naturality, opcyclesOpIso_hom_naturality, π_homologyIsoSc'_hom_assoc, isoHomologyπ_hom, homologyπ_extendHomologyIso_inv_assoc, π_homologyIsoSc'_inv_assoc, isIso_iCycles, cyclesOpIso_hom_naturality_assoc, alternatingConst_iCycles_odd_comp, CochainComplex.isIso_liftCycles_iff, cycles_left_exact, extendCyclesIso_hom_iCycles, homologyπ_singleObjHomologySelfIso_hom, iCyclesIso_hom_inv_id, cyclesOpIso_hom_naturality, liftCycles_i, singleObjCyclesSelfIso_inv_iCycles_assoc, alternatingConst_iCycles_even_comp, toCycles_eq_zero, homology_π_ι_assoc, liftCycles_comp_cyclesMap_assoc, cyclesMap_zero, homologyπ_extendHomologyIso_hom_assoc, toCycles_comp_homologyπ, cyclesFunctor_obj, toCycles_cyclesIsoSc'_hom_assoc, CategoryTheory.ShortComplex.ShortExact.δ_eq, toCycles_comp_homologyπ_assoc, isoHomologyπ_hom_inv_id, extendCyclesIso_hom_naturality, restrictionCyclesIso_inv_iCycles_assoc, CategoryTheory.ShortComplex.ShortExact.δ_apply, cyclesMapIso_inv, singleObjCyclesSelfIso_hom_assoc, singleObjCyclesSelfIso_inv_naturality, π_homologyIsoSc'_inv, cyclesIsoSc'_hom_iCycles, extendCyclesIso_inv_iCycles, restrictionCyclesIso_hom_iCycles_assoc, homology_π_ι, isoHomologyπ_inv_hom_id_assoc, alternatingConst_iCycles_odd_comp_apply, opcyclesToCycles_homologyπ_assoc, extendCyclesIso_hom_iCycles_assoc, opcyclesToCycles_naturality_assoc, singleObjCyclesSelfIso_hom_naturality_assoc, homologyι_opcyclesToCycles, cyclesOpNatIso_hom_app, iCyclesIso_inv_hom_id_assoc, toCycles_cyclesIsoSc'_hom, fromOpcycles_op_cyclesOpIso_inv, pOpcycles_opcyclesToCycles_iCycles, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, pOpcycles_opcyclesToCycles, iCycles_d_assoc, cyclesMap_i, iCyclesIso_hom, isoHomologyπ_hom_inv_id_assoc, pOpcycles_opcyclesToCycles_assoc, opcyclesOpIso_hom_toCycles_op_assoc, singleObjCyclesSelfIso_hom, iCyclesIso_hom_inv_id_assoc, alternatingConst_iCycles_even_comp_assoc, opcyclesToCycles_iCycles, CochainComplex.isIso_homologyπ₀, CochainComplex.liftCycles_shift_homologyπ_assoc, comp_liftCycles_assoc, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv, toCycles_i_assoc, CochainComplex.liftCycles_shift_homologyπ, restrictionCyclesIso_inv_iCycles, cyclesMapIso_hom, homologyπ_restrictionHomologyIso_hom_assoc, liftCycles_homologyπ_eq_zero_of_boundary_assoc, isoHomologyπ_inv_hom_id
|
cyclesFunctor 📖 | CompOp | 11 mathmath: cyclesFunctor_map, HomologySequence.snakeInput_v₂₃, cyclesOpNatIso_inv_app, natTransHomologyπ_app, natTransOpCyclesToCycles_app, HomologySequence.snakeInput_L₂, cyclesFunctor_obj, HomologySequence.snakeInput_v₁₂, HomologySequence.mapSnakeInput_f₂, cyclesOpNatIso_hom_app, instPreservesZeroMorphismsCyclesFunctor
|
cyclesIsKernel 📖 | CompOp | — |
cyclesIsoSc' 📖 | CompOp | 10 mathmath: π_homologyIsoSc'_hom, cyclesIsoSc'_inv_iCycles_assoc, cyclesIsoSc'_hom_iCycles_assoc, cyclesIsoSc'_inv_iCycles, π_homologyIsoSc'_hom_assoc, π_homologyIsoSc'_inv_assoc, toCycles_cyclesIsoSc'_hom_assoc, π_homologyIsoSc'_inv, cyclesIsoSc'_hom_iCycles, toCycles_cyclesIsoSc'_hom
|
cyclesMap 📖 | CompOp | 37 mathmath: liftCycles_comp_cyclesMap, cyclesFunctor_map, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc, CochainComplex.isoHomologyπ₀_inv_naturality_assoc, opcyclesOpIso_inv_naturality_assoc, cyclesMap_comp_assoc, cyclesMap_id, opcyclesOpIso_inv_naturality, cyclesOpIso_inv_naturality_assoc, singleObjCyclesSelfIso_hom_naturality, singleObjCyclesSelfIso_inv_naturality_assoc, cyclesMap_comp, opcyclesToCycles_naturality, CochainComplex.isoHomologyπ₀_inv_naturality, opcyclesOpIso_hom_naturality_assoc, homologyπ_naturality, homologyπ_naturality_assoc, extendCyclesIso_hom_naturality_assoc, truncLE'Map_f_eq_cyclesMap, instMonoCyclesMapOfF, cyclesMap_i_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality, cyclesOpIso_inv_naturality, opcyclesOpIso_hom_naturality, cyclesOpIso_hom_naturality_assoc, cycles_left_exact, cyclesOpIso_hom_naturality, liftCycles_comp_cyclesMap_assoc, cyclesMap_zero, extendCyclesIso_hom_naturality, cyclesMapIso_inv, singleObjCyclesSelfIso_inv_naturality, opcyclesToCycles_naturality_assoc, singleObjCyclesSelfIso_hom_naturality_assoc, HomologySequence.composableArrows₃Functor_map, cyclesMap_i, cyclesMapIso_hom
|
cyclesMapIso 📖 | CompOp | 2 mathmath: cyclesMapIso_inv, cyclesMapIso_hom
|
descOpcycles 📖 | CompOp | 9 mathmath: opcyclesMap_comp_descOpcycles_assoc, descOpcycles_comp, descOpcycles_comp_assoc, ChainComplex.isIso_descOpcycles_iff, opcyclesMap_comp_descOpcycles, homologyι_descOpcycles_eq_zero_of_boundary_assoc, p_descOpcycles_assoc, homologyι_descOpcycles_eq_zero_of_boundary, p_descOpcycles
|
descOpcycles' 📖 | CompOp | — |
fromOpcycles 📖 | CompOp | 16 mathmath: opcyclesIsoSc'_inv_fromOpcycles, opcyclesIsoSc'_inv_fromOpcycles_assoc, p_fromOpcycles, fromOpcycles_d_assoc, fromOpcycles_eq_zero, homologyι_comp_fromOpcycles, opcyclesToCycles_iCycles_assoc, opcyclesOpIso_hom_toCycles_op, fromOpcycles_op_cyclesOpIso_inv_assoc, homologyι_comp_fromOpcycles_assoc, truncGE'_d_eq_fromOpcycles, fromOpcycles_op_cyclesOpIso_inv, p_fromOpcycles_assoc, fromOpcycles_d, opcyclesOpIso_hom_toCycles_op_assoc, opcyclesToCycles_iCycles
|
gradedHomologyFunctor 📖 | CompOp | 2 mathmath: gradedHomologyFunctor_map, gradedHomologyFunctor_obj
|
homology 📖 | CompOp | 135 mathmath: exactAt_iff_isZero_homology, π_homologyIsoSc'_hom, homologyπ_extendHomologyIso_hom, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, isZero_single_obj_homology, homologyπ_restrictionHomologyIso_inv_assoc, homologyι_singleObjOpcyclesSelfIso_inv_assoc, extendHomologyIso_hom_naturality, extendHomologyIso_hom_naturality_assoc, CochainComplex.isoHomologyπ₀_inv_naturality_assoc, CochainComplex.mappingCone.homologySequenceδ_triangleh, eq_liftCycles_homologyπ_up_to_refinements, ChainComplex.isoHomologyι₀_inv_naturality_assoc, isoHomologyι_inv_hom_id, isoHomologyι_hom_inv_id, singleObjCyclesSelfIso_inv_homologyπ, CategoryTheory.ShortComplex.ShortExact.comp_δ, homologyι_singleObjOpcyclesSelfIso_inv, isoOfQuasiIsoAt_hom, extendHomologyIso_hom_homologyι_assoc, homologyπ_extendHomologyIso_inv, homologyπ_restrictionHomologyIso_inv, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom, isoOfQuasiIsoAt_hom_inv_id, homologyι_opcyclesToCycles_assoc, homologyι_comp_fromOpcycles, homologyMap_neg, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homologyπ_singleObjHomologySelfIso_hom_assoc, homologyMapIso_hom, CochainComplex.isoHomologyπ₀_inv_naturality, isoOfQuasiIsoAt_inv_hom_id, isIso_homologyπ, homologyIsoSc'_hom_ι_assoc, restrictionHomologyIso_inv_homologyι_assoc, isoHomologyι_hom, opcyclesToCycles_homologyπ, isIso_homologyMap_shortComplexTruncLE_g, homologyπ_naturality, homologyπ_naturality_assoc, isoOfQuasiIsoAt_inv_hom_id_assoc, instEpiHomologyπ, liftCycles_homologyπ_eq_zero_of_boundary, homologyMap_id, singleObjHomologySelfIso_inv_homologyι_assoc, homologyMap_add, singleObjCyclesSelfIso_inv_homologyπ_assoc, instIsIsoHomologyMapOfQuasiIsoAt, mono_homologyMap_shortComplexTruncLE_g, homologyOp_hom_naturality_assoc, homologyMap_comp, homologyπ_restrictionHomologyIso_hom, π_homologyIsoSc'_hom_assoc, isoHomologyπ_hom, homologyι_comp_fromOpcycles_assoc, restrictionHomologyIso_hom_homologyι, homologyπ_extendHomologyIso_inv_assoc, ChainComplex.isoHomologyι₀_inv_naturality, π_homologyIsoSc'_inv_assoc, instMonoHomologyι, HomologySequence.δ_naturality_assoc, restrictionHomologyIso_hom_homologyι_assoc, homologyMap_sub, homologyπ_singleObjHomologySelfIso_hom, CategoryTheory.ShortComplex.ShortExact.δ_comp_assoc, quasiIsoAt_iff_isIso_homologyMap, CategoryTheory.ShortComplex.ShortExact.homology_exact₃, homology_π_ι_assoc, homologyπ_extendHomologyIso_hom_assoc, homologyMap_zero, toCycles_comp_homologyπ, CategoryTheory.ShortComplex.ShortExact.δ_eq, toCycles_comp_homologyπ_assoc, homologyFunctorSingleIso_inv_app, isoHomologyπ_hom_inv_id, homologyι_naturality, ChainComplex.isIso_homologyι₀, singleObjHomologySelfIso_hom_naturality, gradedHomologyFunctor_obj, CategoryTheory.ShortComplex.ShortExact.δ_apply, homologyIsoSc'_inv_ι, restrictionHomologyIso_inv_homologyι, singleObjHomologySelfIso_hom_naturality_assoc, singleObjHomologySelfIso_inv_naturality_assoc, CochainComplex.isZero_of_isGE, CategoryTheory.ShortComplex.ShortExact.δ_comp, homologyι_descOpcycles_eq_zero_of_boundary_assoc, epi_homologyMap_shortComplexTruncLE_g, epi_homologyMap_of_epi_of_not_rel, CochainComplex.ConnectData.homologyMap_map_of_eq_succ, π_homologyIsoSc'_inv, singleObjHomologySelfIso_inv_naturality, HomologySequence.δ_naturality, homology_π_ι, isoHomologyπ_inv_hom_id_assoc, opcyclesToCycles_homologyπ_assoc, homologyFunctorIso_hom_app, homologyι_opcyclesToCycles, extendHomologyIso_inv_homologyι, homologyIsoSc'_inv_ι_assoc, CategoryTheory.ShortComplex.ShortExact.homology_exact₁, homologyι_descOpcycles_eq_zero_of_boundary, CochainComplex.ConnectData.homologyMap_map_of_eq_neg_succ, isoHomologyι_hom_inv_id_assoc, truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d, ExactAt.isZero_homology, shortComplexTruncLE_shortExact_δ_eq_zero, mono_homologyMap_of_mono_of_not_rel, isoHomologyπ_hom_inv_id_assoc, homologyOp_hom_naturality, homologyIsoSc'_hom_ι, extendHomologyIso_inv_homologyι_assoc, isIso_homologyι, CochainComplex.isIso_homologyπ₀, homologyFunctorIso_inv_app, CochainComplex.liftCycles_shift_homologyπ_assoc, singleObjHomologySelfIso_inv_homologyι, homologyFunctor_obj, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, homologyFunctorSingleIso_hom_app, homologyMap_comp_assoc, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv, isoHomologyι_inv_hom_id_assoc, extendHomologyIso_hom_homologyι, homologyMapIso_inv, CategoryTheory.ShortComplex.ShortExact.homology_exact₂, isoOfQuasiIsoAt_hom_inv_id_assoc, CochainComplex.liftCycles_shift_homologyπ, CochainComplex.isZero_of_isLE, homologyπ_restrictionHomologyIso_hom_assoc, homologyι_naturality_assoc, liftCycles_homologyπ_eq_zero_of_boundary_assoc, CategoryTheory.ShortComplex.ShortExact.comp_δ_assoc, isoHomologyπ_inv_hom_id
|
homologyFunctor 📖 | CompOp | 42 mathmath: CochainComplex.mappingCone.homologySequenceδ_triangleh, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc, HomologySequence.snakeInput_v₂₃, HomologySequence.mapSnakeInput_f₃, CochainComplex.homologyFunctor_shift, natTransHomologyπ_app, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, HomologySequence.snakeInput_v₀₁, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality, instAdditiveHomologyFunctor, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, homologyFunctor_map, instPreservesZeroMorphismsHomologyFunctor, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality, HomologySequence.snakeInput_L₀, CategoryTheory.Functor.leftDerived_map_eq, homologyFunctorSingleIso_inv_app, HomologySequence.snakeInput_L₃, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, HomotopyCategory.homologyFunctor_shiftMap_assoc, CategoryTheory.Functor.rightDerived_map_eq, HomotopyCategory.homologyShiftIso_hom_app, natTransHomologyι_app, homologyFunctorIso_hom_app, HomotopyCategory.homologyFunctor_shiftMap, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc, CochainComplex.ShiftSequence.shiftIso_inv_app, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality, homologyFunctor_inverts_quasiIso, homologyFunctorIso_inv_app, CochainComplex.liftCycles_shift_homologyπ_assoc, homologyFunctor_obj, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, homologyFunctorSingleIso_hom_app, CategoryTheory.InjectiveResolution.rightDerived_app_eq, CochainComplex.liftCycles_shift_homologyπ, HomologySequence.mapSnakeInput_f₀, CochainComplex.ShiftSequence.shiftIso_hom_app
|
homologyFunctorIso 📖 | CompOp | 2 mathmath: homologyFunctorIso_hom_app, homologyFunctorIso_inv_app
|
homologyFunctorIso' 📖 | CompOp | — |
homologyIsCokernel 📖 | CompOp | — |
homologyIsKernel 📖 | CompOp | — |
homologyIsoSc' 📖 | CompOp | 8 mathmath: π_homologyIsoSc'_hom, homologyIsoSc'_hom_ι_assoc, π_homologyIsoSc'_hom_assoc, π_homologyIsoSc'_inv_assoc, homologyIsoSc'_inv_ι, π_homologyIsoSc'_inv, homologyIsoSc'_inv_ι_assoc, homologyIsoSc'_hom_ι
|
homologyMap 📖 | CompOp | 53 mathmath: Homotopy.homologyMap_eq, extendHomologyIso_hom_naturality, extendHomologyIso_hom_naturality_assoc, CochainComplex.isoHomologyπ₀_inv_naturality_assoc, CochainComplex.mappingCone.homologySequenceδ_triangleh, ChainComplex.isoHomologyι₀_inv_naturality_assoc, CategoryTheory.ShortComplex.ShortExact.comp_δ, isoOfQuasiIsoAt_hom, isoOfQuasiIsoAt_hom_inv_id, gradedHomologyFunctor_map, homologyMap_neg, homologyMapIso_hom, CochainComplex.isoHomologyπ₀_inv_naturality, isoOfQuasiIsoAt_inv_hom_id, isIso_homologyMap_shortComplexTruncLE_g, homologyπ_naturality, homologyπ_naturality_assoc, isoOfQuasiIsoAt_inv_hom_id_assoc, homologyMap_id, homologyMap_add, instIsIsoHomologyMapOfQuasiIsoAt, mono_homologyMap_shortComplexTruncLE_g, homologyOp_hom_naturality_assoc, homologyMap_comp, ChainComplex.isoHomologyι₀_inv_naturality, homologyFunctor_map, HomologySequence.δ_naturality_assoc, homologyMap_sub, CategoryTheory.ShortComplex.ShortExact.δ_comp_assoc, quasiIsoAt_iff_isIso_homologyMap, CategoryTheory.ShortComplex.ShortExact.homology_exact₃, homologyMap_zero, homologyι_naturality, singleObjHomologySelfIso_hom_naturality, singleObjHomologySelfIso_hom_naturality_assoc, singleObjHomologySelfIso_inv_naturality_assoc, CategoryTheory.ShortComplex.ShortExact.δ_comp, epi_homologyMap_shortComplexTruncLE_g, epi_homologyMap_of_epi_of_not_rel, CochainComplex.ConnectData.homologyMap_map_of_eq_succ, singleObjHomologySelfIso_inv_naturality, HomologySequence.δ_naturality, HomologySequence.composableArrows₃Functor_map, CategoryTheory.ShortComplex.ShortExact.homology_exact₁, CochainComplex.ConnectData.homologyMap_map_of_eq_neg_succ, mono_homologyMap_of_mono_of_not_rel, homologyOp_hom_naturality, homologyMap_comp_assoc, homologyMapIso_inv, CategoryTheory.ShortComplex.ShortExact.homology_exact₂, isoOfQuasiIsoAt_hom_inv_id_assoc, homologyι_naturality_assoc, CategoryTheory.ShortComplex.ShortExact.comp_δ_assoc
|
homologyMapIso 📖 | CompOp | 2 mathmath: homologyMapIso_hom, homologyMapIso_inv
|
homologyι 📖 | CompOp | 38 mathmath: singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, homologyι_singleObjOpcyclesSelfIso_inv_assoc, isoHomologyι_inv_hom_id, isoHomologyι_hom_inv_id, homologyι_singleObjOpcyclesSelfIso_inv, extendHomologyIso_hom_homologyι_assoc, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom, homologyι_opcyclesToCycles_assoc, homologyι_comp_fromOpcycles, homologyIsoSc'_hom_ι_assoc, restrictionHomologyIso_inv_homologyι_assoc, isoHomologyι_hom, singleObjHomologySelfIso_inv_homologyι_assoc, homologyι_comp_fromOpcycles_assoc, restrictionHomologyIso_hom_homologyι, instMonoHomologyι, restrictionHomologyIso_hom_homologyι_assoc, homology_π_ι_assoc, homologyι_naturality, ChainComplex.isIso_homologyι₀, homologyIsoSc'_inv_ι, restrictionHomologyIso_inv_homologyι, homologyι_descOpcycles_eq_zero_of_boundary_assoc, homology_π_ι, natTransHomologyι_app, homologyι_opcyclesToCycles, extendHomologyIso_inv_homologyι, homologyIsoSc'_inv_ι_assoc, homologyι_descOpcycles_eq_zero_of_boundary, isoHomologyι_hom_inv_id_assoc, truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d, homologyIsoSc'_hom_ι, extendHomologyIso_inv_homologyι_assoc, isIso_homologyι, singleObjHomologySelfIso_inv_homologyι, isoHomologyι_inv_hom_id_assoc, extendHomologyIso_hom_homologyι, homologyι_naturality_assoc
|
homologyπ 📖 | CompOp | 44 mathmath: π_homologyIsoSc'_hom, homologyπ_extendHomologyIso_hom, homologyπ_restrictionHomologyIso_inv_assoc, eq_liftCycles_homologyπ_up_to_refinements, singleObjCyclesSelfIso_inv_homologyπ, homologyπ_extendHomologyIso_inv, homologyπ_restrictionHomologyIso_inv, CategoryTheory.ShortComplex.ShortExact.δ_eq', natTransHomologyπ_app, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homologyπ_singleObjHomologySelfIso_hom_assoc, isIso_homologyπ, opcyclesToCycles_homologyπ, homologyπ_naturality, homologyπ_naturality_assoc, instEpiHomologyπ, liftCycles_homologyπ_eq_zero_of_boundary, singleObjCyclesSelfIso_inv_homologyπ_assoc, homologyπ_restrictionHomologyIso_hom, π_homologyIsoSc'_hom_assoc, isoHomologyπ_hom, homologyπ_extendHomologyIso_inv_assoc, CategoryTheory.ShortComplex.ShortExact.δ_apply', π_homologyIsoSc'_inv_assoc, homologyπ_singleObjHomologySelfIso_hom, homology_π_ι_assoc, homologyπ_extendHomologyIso_hom_assoc, toCycles_comp_homologyπ, CategoryTheory.ShortComplex.ShortExact.δ_eq, toCycles_comp_homologyπ_assoc, isoHomologyπ_hom_inv_id, CategoryTheory.ShortComplex.ShortExact.δ_apply, π_homologyIsoSc'_inv, homology_π_ι, isoHomologyπ_inv_hom_id_assoc, opcyclesToCycles_homologyπ_assoc, isoHomologyπ_hom_inv_id_assoc, CochainComplex.isIso_homologyπ₀, CochainComplex.liftCycles_shift_homologyπ_assoc, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv, CochainComplex.liftCycles_shift_homologyπ, homologyπ_restrictionHomologyIso_hom_assoc, liftCycles_homologyπ_eq_zero_of_boundary_assoc, isoHomologyπ_inv_hom_id
|
iCycles 📖 | CompOp | 48 mathmath: singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, alternatingConst_iCycles_odd_comp_assoc, pOpcycles_opcyclesToCycles_iCycles_assoc, singleObjCyclesSelfIso_inv_iCycles, toCycles_i, instMonoICycles, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, restrictionCyclesIso_hom_iCycles, iCyclesIso_inv_hom_id, extendCyclesIso_inv_iCycles_assoc, cyclesIsoSc'_inv_iCycles_assoc, opcyclesToCycles_iCycles_assoc, iCycles_d, cyclesIsoSc'_hom_iCycles_assoc, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, alternatingConst_iCycles_even_comp_apply, cyclesIsoSc'_inv_iCycles, cyclesMap_i_assoc, liftCycles_i_assoc, i_cyclesMk, isIso_iCycles, alternatingConst_iCycles_odd_comp, extendCyclesIso_hom_iCycles, iCyclesIso_hom_inv_id, liftCycles_i, singleObjCyclesSelfIso_inv_iCycles_assoc, alternatingConst_iCycles_even_comp, homology_π_ι_assoc, restrictionCyclesIso_inv_iCycles_assoc, singleObjCyclesSelfIso_hom_assoc, cyclesIsoSc'_hom_iCycles, extendCyclesIso_inv_iCycles, restrictionCyclesIso_hom_iCycles_assoc, homology_π_ι, alternatingConst_iCycles_odd_comp_apply, extendCyclesIso_hom_iCycles_assoc, iCyclesIso_inv_hom_id_assoc, pOpcycles_opcyclesToCycles_iCycles, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, iCycles_d_assoc, cyclesMap_i, iCyclesIso_hom, singleObjCyclesSelfIso_hom, iCyclesIso_hom_inv_id_assoc, alternatingConst_iCycles_even_comp_assoc, opcyclesToCycles_iCycles, toCycles_i_assoc, restrictionCyclesIso_inv_iCycles
|
iCyclesIso 📖 | CompOp | 5 mathmath: iCyclesIso_inv_hom_id, iCyclesIso_hom_inv_id, iCyclesIso_inv_hom_id_assoc, iCyclesIso_hom, iCyclesIso_hom_inv_id_assoc
|
isoHomologyι 📖 | CompOp | 5 mathmath: isoHomologyι_inv_hom_id, isoHomologyι_hom_inv_id, isoHomologyι_hom, isoHomologyι_hom_inv_id_assoc, isoHomologyι_inv_hom_id_assoc
|
isoHomologyπ 📖 | CompOp | 5 mathmath: isoHomologyπ_hom, isoHomologyπ_hom_inv_id, isoHomologyπ_inv_hom_id_assoc, isoHomologyπ_hom_inv_id_assoc, isoHomologyπ_inv_hom_id
|
isoSc' 📖 | CompOp | — |
liftCycles 📖 | CompOp | 13 mathmath: liftCycles_comp_cyclesMap, eq_liftCycles_homologyπ_up_to_refinements, comp_liftCycles, liftCycles_homologyπ_eq_zero_of_boundary, liftCycles_i_assoc, CochainComplex.isIso_liftCycles_iff, liftCycles_i, liftCycles_comp_cyclesMap_assoc, CategoryTheory.ShortComplex.ShortExact.δ_eq, CochainComplex.liftCycles_shift_homologyπ_assoc, comp_liftCycles_assoc, CochainComplex.liftCycles_shift_homologyπ, liftCycles_homologyπ_eq_zero_of_boundary_assoc
|
liftCycles' 📖 | CompOp | — |
natIsoSc' 📖 | CompOp | 14 mathmath: natIsoSc'_inv_app_τ₂, natIsoSc'_inv_app_τ₃, natIsoSc'_hom_app_τ₃, groupHomology.isoShortComplexH1_hom, natIsoSc'_hom_app_τ₂, groupHomology.isoShortComplexH1_inv, groupHomology.isoShortComplexH2_hom, groupCohomology.isoShortComplexH1_hom, groupCohomology.isoShortComplexH2_hom, groupHomology.isoShortComplexH2_inv, groupCohomology.isoShortComplexH1_inv, groupCohomology.isoShortComplexH2_inv, natIsoSc'_inv_app_τ₁, natIsoSc'_hom_app_τ₁
|
natTransHomologyι 📖 | CompOp | 2 mathmath: HomologySequence.snakeInput_v₀₁, natTransHomologyι_app
|
natTransHomologyπ 📖 | CompOp | 2 mathmath: HomologySequence.snakeInput_v₂₃, natTransHomologyπ_app
|
opcycles 📖 | CompOp | 137 mathmath: pOpcycles_restrictionOpcyclesIso_hom_assoc, opcyclesMap_comp_descOpcycles_assoc, restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, truncGE.rightHomologyMapData_φQ, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, opcyclesMap_comp, pOpcycles_opcyclesToCycles_iCycles_assoc, pOpcycles_opcyclesIsoSc'_hom, pOpcycles_singleObjOpcyclesSelfIso_inv, opcyclesIsoSc'_inv_fromOpcycles, singleObjOpcyclesSelfIso_hom, opcyclesMapIso_inv, pOpcyclesIso_hom, homologyι_singleObjOpcyclesSelfIso_inv_assoc, instEpiOpcyclesMapOfF, opcyclesOpIso_inv_naturality_assoc, opcyclesIsoSc'_inv_fromOpcycles_assoc, p_fromOpcycles, ChainComplex.isoHomologyι₀_inv_naturality_assoc, isoHomologyι_inv_hom_id, isoHomologyι_hom_inv_id, pOpcycles_opcyclesIsoSc'_inv_assoc, opcyclesOpIso_inv_naturality, homologyι_singleObjOpcyclesSelfIso_inv, extendHomologyIso_hom_homologyι_assoc, fromOpcycles_d_assoc, pOpcycles_opcyclesIsoSc'_inv, cyclesOpIso_inv_naturality_assoc, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom, d_pOpcycles, fromOpcycles_eq_zero, opcyclesMap_id, homologyι_opcyclesToCycles_assoc, pOpcycles_restrictionOpcyclesIso_inv, cyclesOpNatIso_inv_app, homologyι_comp_fromOpcycles, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, opcyclesMapIso_hom, opcyclesToCycles_iCycles_assoc, descOpcycles_comp, opcyclesToCycles_naturality, homologyIsoSc'_hom_ι_assoc, restrictionHomologyIso_inv_homologyι_assoc, isoHomologyι_hom, opcyclesOpIso_hom_naturality_assoc, opcyclesToCycles_homologyπ, p_opcyclesMap, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, descOpcycles_comp_assoc, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, opcyclesOpIso_hom_toCycles_op, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, pOpcyclesIso_inv_hom_id, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, d_pOpcycles_assoc, singleObjHomologySelfIso_inv_homologyι_assoc, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', ChainComplex.isIso_descOpcycles_iff, fromOpcycles_op_cyclesOpIso_inv_assoc, singleObjOpcyclesSelfIso_inv_naturality, cyclesOpIso_inv_naturality, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality, opcyclesOpIso_hom_naturality, opcycles_right_exact, homologyι_comp_fromOpcycles_assoc, opcyclesMap_comp_assoc, restrictionHomologyIso_hom_homologyι, ChainComplex.isoHomologyι₀_inv_naturality, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc, cyclesOpIso_hom_naturality_assoc, instMonoHomologyι, opcyclesMap_comp_descOpcycles, truncGE'_d_eq_fromOpcycles, restrictionHomologyIso_hom_homologyι_assoc, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, cyclesOpIso_hom_naturality, singleObjOpcyclesSelfIso_hom_naturality_assoc, pOpcycles_extendOpcyclesIso_hom_assoc, pOpcycles_extendOpcyclesIso_inv, homology_π_ι_assoc, truncGE'Map_f_eq_opcyclesMap, restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv, isIso_pOpcycles, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, homologyι_naturality, ChainComplex.isIso_homologyι₀, homologyIsoSc'_inv_ι, restrictionHomologyIso_inv_homologyι, pOpcyclesIso_hom_inv_id_assoc, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, pOpcycles_opcyclesIsoSc'_hom_assoc, pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, homologyι_descOpcycles_eq_zero_of_boundary_assoc, p_descOpcycles_assoc, singleObjOpcyclesSelfIso_inv_naturality_assoc, pOpcycles_extendOpcyclesIso_hom, homology_π_ι, opcyclesToCycles_homologyπ_assoc, opcyclesFunctor_obj, opcyclesToCycles_naturality_assoc, homologyι_opcyclesToCycles, cyclesOpNatIso_hom_app, fromOpcycles_op_cyclesOpIso_inv, pOpcycles_opcyclesToCycles_iCycles, p_fromOpcycles_assoc, extendHomologyIso_inv_homologyι, pOpcycles_opcyclesToCycles, homologyIsoSc'_inv_ι_assoc, homologyι_descOpcycles_eq_zero_of_boundary, fromOpcycles_d, isoHomologyι_hom_inv_id_assoc, pOpcyclesIso_inv_hom_id_assoc, truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d, opcyclesMap_zero, instEpiPOpcycles, pOpcycles_restrictionOpcyclesIso_inv_assoc, homologyIsoSc'_hom_ι, extendHomologyIso_inv_homologyι_assoc, pOpcycles_extendOpcyclesIso_inv_assoc, pOpcycles_opcyclesToCycles_assoc, opcyclesOpIso_hom_toCycles_op_assoc, pOpcyclesIso_hom_inv_id, isIso_homologyι, opcyclesToCycles_iCycles, singleObjHomologySelfIso_inv_homologyι, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, singleObjOpcyclesSelfIso_hom_assoc, isoHomologyι_inv_hom_id_assoc, singleObjOpcyclesSelfIso_hom_naturality, extendHomologyIso_hom_homologyι, p_opcyclesMap_assoc, p_descOpcycles, homologyι_naturality_assoc, pOpcycles_restrictionOpcyclesIso_hom, CategoryTheory.instIsIsoFromLeftDerivedZero'
|
opcyclesFunctor 📖 | CompOp | 11 mathmath: HomologySequence.snakeInput_L₁, cyclesOpNatIso_inv_app, opcyclesFunctor_map, HomologySequence.snakeInput_v₀₁, HomologySequence.mapSnakeInput_f₁, natTransOpCyclesToCycles_app, HomologySequence.snakeInput_v₁₂, opcyclesFunctor_obj, natTransHomologyι_app, cyclesOpNatIso_hom_app, instPreservesZeroMorphismsOpcyclesFunctor
|
opcyclesIsCokernel 📖 | CompOp | — |
opcyclesIsoSc' 📖 | CompOp | 10 mathmath: pOpcycles_opcyclesIsoSc'_hom, opcyclesIsoSc'_inv_fromOpcycles, opcyclesIsoSc'_inv_fromOpcycles_assoc, pOpcycles_opcyclesIsoSc'_inv_assoc, pOpcycles_opcyclesIsoSc'_inv, homologyIsoSc'_hom_ι_assoc, homologyIsoSc'_inv_ι, pOpcycles_opcyclesIsoSc'_hom_assoc, homologyIsoSc'_inv_ι_assoc, homologyIsoSc'_hom_ι
|
opcyclesMap 📖 | CompOp | 35 mathmath: opcyclesMap_comp_descOpcycles_assoc, opcyclesMap_comp, opcyclesMapIso_inv, instEpiOpcyclesMapOfF, opcyclesOpIso_inv_naturality_assoc, ChainComplex.isoHomologyι₀_inv_naturality_assoc, opcyclesOpIso_inv_naturality, cyclesOpIso_inv_naturality_assoc, opcyclesMap_id, opcyclesFunctor_map, opcyclesMapIso_hom, opcyclesToCycles_naturality, opcyclesOpIso_hom_naturality_assoc, p_opcyclesMap, singleObjOpcyclesSelfIso_inv_naturality, cyclesOpIso_inv_naturality, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality, opcyclesOpIso_hom_naturality, opcycles_right_exact, opcyclesMap_comp_assoc, ChainComplex.isoHomologyι₀_inv_naturality, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc, cyclesOpIso_hom_naturality_assoc, opcyclesMap_comp_descOpcycles, cyclesOpIso_hom_naturality, singleObjOpcyclesSelfIso_hom_naturality_assoc, truncGE'Map_f_eq_opcyclesMap, homologyι_naturality, singleObjOpcyclesSelfIso_inv_naturality_assoc, opcyclesToCycles_naturality_assoc, HomologySequence.composableArrows₃Functor_map, opcyclesMap_zero, singleObjOpcyclesSelfIso_hom_naturality, p_opcyclesMap_assoc, homologyι_naturality_assoc
|
opcyclesMapIso 📖 | CompOp | 2 mathmath: opcyclesMapIso_inv, opcyclesMapIso_hom
|
pOpcycles 📖 | CompOp | 49 mathmath: pOpcycles_restrictionOpcyclesIso_hom_assoc, restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, pOpcycles_opcyclesToCycles_iCycles_assoc, pOpcycles_opcyclesIsoSc'_hom, pOpcycles_singleObjOpcyclesSelfIso_inv, singleObjOpcyclesSelfIso_hom, pOpcyclesIso_hom, p_fromOpcycles, pOpcycles_opcyclesIsoSc'_inv_assoc, pOpcycles_opcyclesIsoSc'_inv, d_pOpcycles, pOpcycles_restrictionOpcyclesIso_inv, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, p_opcyclesMap, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, pOpcyclesIso_inv_hom_id, d_pOpcycles_assoc, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, pOpcycles_extendOpcyclesIso_hom_assoc, pOpcycles_extendOpcyclesIso_inv, homology_π_ι_assoc, restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv, isIso_pOpcycles, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, pOpcyclesIso_hom_inv_id_assoc, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, pOpcycles_opcyclesIsoSc'_hom_assoc, pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, p_descOpcycles_assoc, pOpcycles_extendOpcyclesIso_hom, homology_π_ι, pOpcycles_opcyclesToCycles_iCycles, p_fromOpcycles_assoc, pOpcycles_opcyclesToCycles, pOpcyclesIso_inv_hom_id_assoc, instEpiPOpcycles, pOpcycles_restrictionOpcyclesIso_inv_assoc, pOpcycles_extendOpcyclesIso_inv_assoc, pOpcycles_opcyclesToCycles_assoc, pOpcyclesIso_hom_inv_id, singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap_assoc, p_descOpcycles, pOpcycles_restrictionOpcyclesIso_hom
|
pOpcyclesIso 📖 | CompOp | 5 mathmath: pOpcyclesIso_hom, pOpcyclesIso_inv_hom_id, pOpcyclesIso_hom_inv_id_assoc, pOpcyclesIso_inv_hom_id_assoc, pOpcyclesIso_hom_inv_id
|
sc 📖 | CompOp | 91 mathmath: truncGE.rightHomologyMapData_φQ, alternatingConst_iCycles_odd_comp_assoc, extend.homologyData'_left_H, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc, CochainComplex.mappingCone.homologySequenceδ_triangleh, eq_liftCycles_homologyπ_up_to_refinements, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, CochainComplex.HomComplex.leftHomologyData_K_coe, CategoryTheory.ShortComplex.ShortExact.comp_δ, mem_quasiIso_iff, CategoryTheory.instIsIsoToRightDerivedZero', CochainComplex.HomComplex.leftHomologyData_π_hom_apply, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CochainComplex.HomComplex.leftHomologyData_i_hom_apply, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, quasiIso_iff_evaluation, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self, isIso_homologyMap_shortComplexTruncLE_g, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, HomologySequence.quasiIso_τ₃, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, exactAt_iff, groupHomology.isoShortComplexH1_hom, alternatingConst_iCycles_even_comp_apply, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', CochainComplex.quasiIso_shift_iff, g_shortComplexTruncLEX₃ToTruncGE, mono_homologyMap_shortComplexTruncLE_g, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality, i_cyclesMk, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality, quasiIsoAt_shortComplexTruncLE_g, extend.homologyData'_right_H, CochainComplex.quasiIsoAt_shift_iff, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc, extend.homologyData'_iso, HomologySequence.δ_naturality_assoc, alternatingConst_iCycles_odd_comp, groupHomology.isoShortComplexH1_inv, extend.homologyData'_right_p, extend.homologyData'_left_i, CochainComplex.cm5b.instQuasiIsoIntP, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, CochainComplex.mappingCone.quasiIso_descShortComplex, CategoryTheory.ShortComplex.ShortExact.δ_comp_assoc, alternatingConst_iCycles_even_comp, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, CategoryTheory.ShortComplex.ShortExact.homology_exact₃, CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor, groupHomology.isoShortComplexH2_hom, CategoryTheory.ShortComplex.ShortExact.δ_eq, groupHomology.pOpcycles_comp_opcyclesIso_hom, quasiIsoAt_iff_evaluation, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, truncGE.rightHomologyMapData_φH, groupCohomology.isoShortComplexH1_hom, extend.homologyData'_right_ι, CochainComplex.HomComplex.leftHomologyData_H_coe, CategoryTheory.ShortComplex.ShortExact.δ_apply, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, CategoryTheory.ShortComplex.ShortExact.δ_comp, Rep.standardComplex.instQuasiIsoNatεToSingle₀, epi_homologyMap_shortComplexTruncLE_g, CategoryTheory.InjectiveResolution.instQuasiIsoIntι', Rep.FiniteCyclicGroup.resolution_quasiIso, extend.homologyData'_right_Q, HomologySequence.δ_naturality, groupCohomology.isoShortComplexH2_hom, alternatingConst_iCycles_odd_comp_apply, CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ', CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, HomologySequence.composableArrows₃_exact, groupHomology.isoShortComplexH2_inv, extend.homologyData'_left_π, extend.homologyData'_left_K, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, CategoryTheory.ShortComplex.ShortExact.homology_exact₁, instQuasiIsoShortComplexTruncLEX₃ToTruncGE, groupCohomology.isoShortComplexH1_inv, shortComplexTruncLE_shortExact_δ_eq_zero, alternatingConst_iCycles_even_comp_assoc, DerivedCategory.isIso_Q_map_iff_quasiIso, groupCohomology.isoShortComplexH2_inv, CochainComplex.liftCycles_shift_homologyπ_assoc, g_shortComplexTruncLEX₃ToTruncGE_assoc, CategoryTheory.ShortComplex.ShortExact.homology_exact₂, CochainComplex.liftCycles_shift_homologyπ, CategoryTheory.instIsIsoFromLeftDerivedZero', CategoryTheory.ShortComplex.ShortExact.comp_δ_assoc
|
sc' 📖 | CompOp | 64 mathmath: π_homologyIsoSc'_hom, truncGE.rightHomologyMapData_φQ, pOpcycles_opcyclesIsoSc'_hom, extend.leftHomologyData_π, opcyclesIsoSc'_inv_fromOpcycles, extend.homologyData_left, extend.homologyData'_left_H, restriction.sc'Iso_inv_τ₃, opcyclesIsoSc'_inv_fromOpcycles_assoc, CochainComplex.HomComplex.leftHomologyData'_i, pOpcycles_opcyclesIsoSc'_inv_assoc, pOpcycles_opcyclesIsoSc'_inv, restriction.sc'Iso_inv_τ₁, cyclesIsoSc'_inv_iCycles_assoc, homologyIsoSc'_hom_ι_assoc, cyclesIsoSc'_hom_iCycles_assoc, restriction.sc'Iso_hom_τ₂, groupHomology.isoShortComplexH1_hom, cyclesIsoSc'_inv_iCycles, truncGE'.hasHomology_sc'_of_not_mem_boundary, truncGE'.homologyData_right_g', π_homologyIsoSc'_hom_assoc, extend.homologyData'_right_H, extend.rightHomologyData_p, π_homologyIsoSc'_inv_assoc, extend.leftHomologyData_H, extend.homologyData'_iso, extend.rightHomologyData_g', extend.rightHomologyData_ι, groupHomology.isoShortComplexH1_inv, extend.homologyData'_right_p, extend.homologyData'_left_i, groupHomology.isoShortComplexH2_hom, toCycles_cyclesIsoSc'_hom_assoc, extend.rightHomologyData_H, truncGE.rightHomologyMapData_φH, groupCohomology.isoShortComplexH1_hom, extend.homologyData'_right_ι, extend.leftHomologyData_i, CochainComplex.HomComplex.leftHomologyData'_K_coe, homologyIsoSc'_inv_ι, pOpcycles_opcyclesIsoSc'_hom_assoc, extend.homologyData'_right_Q, CochainComplex.HomComplex.leftHomologyData'_H_coe, π_homologyIsoSc'_inv, cyclesIsoSc'_hom_iCycles, extend.leftHomologyData_K, groupCohomology.isoShortComplexH2_hom, restriction.sc'Iso_inv_τ₂, CochainComplex.HomComplex.leftHomologyData'_π, groupHomology.isoShortComplexH2_inv, toCycles_cyclesIsoSc'_hom, extend.homologyData'_left_π, extend.homologyData'_left_K, extend.homologyData_iso, homologyIsoSc'_inv_ι_assoc, groupCohomology.isoShortComplexH1_inv, homologyIsoSc'_hom_ι, extend.homologyData_right, restriction.sc'Iso_hom_τ₃, groupCohomology.isoShortComplexH2_inv, exactAt_iff', extend.rightHomologyData_Q, restriction.sc'Iso_hom_τ₁
|
shortComplexFunctor 📖 | CompOp | 38 mathmath: truncGE.rightHomologyMapData_φQ, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, CochainComplex.shiftShortComplexFunctorIso_add'_hom_app, natIsoSc'_inv_app_τ₂, natIsoSc'_inv_app_τ₃, natIsoSc'_hom_app_τ₃, shortComplexFunctor_obj_X₂, groupHomology.isoShortComplexH1_hom, shortComplexFunctor_map_τ₁, shortComplexFunctor_map_τ₃, shortComplexFunctor_obj_f, natIsoSc'_hom_app_τ₂, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, QuasiIsoAt.quasiIso, groupHomology.isoShortComplexH1_inv, groupHomology.isoShortComplexH2_hom, shortComplexFunctor_obj_X₁, truncGE.rightHomologyMapData_φH, groupCohomology.isoShortComplexH1_hom, groupCohomology.isoShortComplexH2_hom, homologyFunctorIso_hom_app, shortComplexFunctor_map_τ₂, shortComplexFunctor_obj_g, groupHomology.isoShortComplexH2_inv, quasiIsoAt_iff, CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, groupCohomology.isoShortComplexH1_inv, CochainComplex.ShiftSequence.shiftIso_inv_app, groupCohomology.isoShortComplexH2_inv, homologyFunctorIso_inv_app, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, natIsoSc'_inv_app_τ₁, natIsoSc'_hom_app_τ₁, shortComplexFunctor_obj_X₃, CochainComplex.ShiftSequence.shiftIso_hom_app
|
shortComplexFunctor' 📖 | CompOp | 37 mathmath: shortComplexFunctor'_obj_X₁, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, natIsoSc'_inv_app_τ₂, shortComplexFunctor'_map_τ₂, natIsoSc'_inv_app_τ₃, natIsoSc'_hom_app_τ₃, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, ChainComplex.quasiIsoAt₀_iff, groupHomology.isoShortComplexH1_hom, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂, shortComplexFunctor'_obj_X₂, shortComplexFunctor'_obj_X₃, shortComplexFunctor'_obj_g, natIsoSc'_hom_app_τ₂, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, groupHomology.isoShortComplexH1_inv, shortComplexFunctor'_map_τ₁, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, groupHomology.isoShortComplexH2_hom, groupCohomology.isoShortComplexH1_hom, quasiIsoAt_iff', CochainComplex.quasiIsoAt₀_iff, groupCohomology.isoShortComplexH2_hom, shortComplexFunctor'_map_τ₃, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, groupHomology.isoShortComplexH2_inv, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂, shortComplexFunctor'_obj_f, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, groupCohomology.isoShortComplexH1_inv, groupCohomology.isoShortComplexH2_inv, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, natIsoSc'_inv_app_τ₁, natIsoSc'_hom_app_τ₁
|
toCycles 📖 | CompOp | 16 mathmath: toCycles_i, truncLE'_d_eq_toCycles, d_toCycles_assoc, opcyclesOpIso_hom_toCycles_op, d_toCycles, fromOpcycles_op_cyclesOpIso_inv_assoc, toCycles_eq_zero, toCycles_comp_homologyπ, toCycles_cyclesIsoSc'_hom_assoc, toCycles_comp_homologyπ_assoc, toCycles_cyclesIsoSc'_hom, fromOpcycles_op_cyclesOpIso_inv, pOpcycles_opcyclesToCycles, pOpcycles_opcyclesToCycles_assoc, opcyclesOpIso_hom_toCycles_op_assoc, toCycles_i_assoc
|