CategoryTheory.AdditiveEuler.cochain_shift_term_sum |
theorem |
HomologicalAlgebra/AdditiveEuler/Shift.lean, line 110 |
|
CategoryTheory.AdditiveEuler.cochainShiftHomologyIso |
def |
HomologicalAlgebra/AdditiveEuler/Shift.lean, line 119 |
|
CategoryTheory.AdditiveEuler.cochain_shift_homology_sum |
theorem |
HomologicalAlgebra/AdditiveEuler/Shift.lean, line 135 |
|
CategoryTheory.AdditiveEuler.cochain_euler_endpoints |
theorem |
HomologicalAlgebra/AdditiveEuler/Cochain.lean, line 54 |
|
CategoryTheory.AdditiveEuler.cochain_euler_eq_homology |
theorem |
HomologicalAlgebra/AdditiveEuler/Cochain.lean, line 77 |
|
CategoryTheory.AdditiveEuler.cochain_euler_eq_homology_of_bounded |
theorem |
HomologicalAlgebra/AdditiveEuler/Cochain.lean, line 86 |
|
CategoryTheory.AdditiveEuler.cochain_euler_acyclic |
theorem |
HomologicalAlgebra/AdditiveEuler/Cochain.lean, line 96 |
|
CategoryTheory.AdditiveEuler.cochain_euler_quasiIso |
theorem |
HomologicalAlgebra/AdditiveEuler/Cochain.lean, line 107 |
|
CategoryTheory.AdditiveEuler.invariant_exact_pair_images |
theorem |
HomologicalAlgebra/AdditiveEuler/HomologySupport.lean, line 41 |
|
CategoryTheory.AdditiveEuler.cochain_homology_local_additivity |
theorem |
HomologicalAlgebra/AdditiveEuler/HomologySupport.lean, line 73 |
|
CategoryTheory.AdditiveEuler.cochain_homology_euler_endpoints |
theorem |
HomologicalAlgebra/AdditiveEuler/HomologySupport.lean, line 111 |
|
CategoryTheory.AdditiveEuler.cochain_homology_sum_additive_of_endpoints |
theorem |
HomologicalAlgebra/AdditiveEuler/HomologySupport.lean, line 137 |
|
CategoryTheory.AdditiveEuler.cochain_homology_sum_additive_of_supported |
theorem |
HomologicalAlgebra/AdditiveEuler/HomologySupport.lean, line 155 |
|
HomologicalComplex.cylinder.ι₀_comp_πCompι₀Homotopy_hom |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 30 |
|
CochainComplex.RelativePath.path_hom_π₀ |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 56 |
|
CochainComplex.RelativePath.obj |
def |
HomologicalAlgebra/Cochain/RelativePath.lean, line 73 |
|
CochainComplex.RelativePath.fst |
def |
HomologicalAlgebra/Cochain/RelativePath.lean, line 77 |
|
CochainComplex.RelativePath.snd |
def |
HomologicalAlgebra/Cochain/RelativePath.lean, line 81 |
|
CochainComplex.RelativePath.toTarget |
def |
HomologicalAlgebra/Cochain/RelativePath.lean, line 85 |
|
CochainComplex.RelativePath.sectionMap |
def |
HomologicalAlgebra/Cochain/RelativePath.lean, line 89 |
|
CochainComplex.RelativePath.section_fst |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 92 |
|
CochainComplex.RelativePath.section_snd |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 95 |
|
CochainComplex.RelativePath.section_toTarget |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 99 |
|
CochainComplex.RelativePath.fst_comp |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 104 |
|
CochainComplex.RelativePath.lift |
def |
HomologicalAlgebra/Cochain/RelativePath.lean, line 109 |
|
CochainComplex.RelativePath.lift_fst |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 113 |
|
CochainComplex.RelativePath.lift_toTarget |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 117 |
|
CochainComplex.RelativePath.isPullbackAt |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 122 |
|
CochainComplex.RelativePath.contraction |
def |
HomologicalAlgebra/Cochain/RelativePath.lean, line 179 |
|
CochainComplex.RelativePath.contraction_fst_hom |
theorem |
HomologicalAlgebra/Cochain/RelativePath.lean, line 208 |
|
CochainComplex.RelativePath.equivalence |
def |
HomologicalAlgebra/Cochain/RelativePath.lean, line 213 |
|
CochainComplex.RelativePath.comparison |
def |
HomologicalAlgebra/Cochain/RelativePath.lean, line 220 |
|
CategoryTheory.Subobject.quotientIntersectionPair |
def |
HomologicalAlgebra/Abelian/QuotientIntersection.lean, line 46 |
|
CategoryTheory.Subobject.quotientIntersectionPair_fst |
theorem |
HomologicalAlgebra/Abelian/QuotientIntersection.lean, line 58 |
|
CategoryTheory.Subobject.quotientIntersectionPair_snd |
theorem |
HomologicalAlgebra/Abelian/QuotientIntersection.lean, line 66 |
|
CategoryTheory.Subobject.quotientIntersectionPair_fac |
theorem |
HomologicalAlgebra/Abelian/QuotientIntersection.lean, line 74 |
|
CategoryTheory.Subobject.mono_quotientIntersectionPair |
instance |
HomologicalAlgebra/Abelian/QuotientIntersection.lean, line 129 |
|
CategoryTheory.QuadrantProductTotal.Bicomplex |
abbrev |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 34 |
|
CategoryTheory.QuadrantProductTotal.Diag |
abbrev |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 38 |
|
CategoryTheory.QuadrantProductTotal.firstRow |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 41 |
|
CategoryTheory.QuadrantProductTotal.firstColumn |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 44 |
|
CategoryTheory.QuadrantProductTotal.diagonalIndex |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 47 |
|
CategoryTheory.QuadrantProductTotal.primitiveIndex |
abbrev |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 53 |
|
CategoryTheory.QuadrantProductTotal.diagonalIndex_surjective |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 58 |
|
CategoryTheory.QuadrantProductTotal.primitiveIndex_of_row |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 68 |
|
CategoryTheory.QuadrantProductTotal.cycleIndex |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 81 |
|
CategoryTheory.QuadrantProductTotal.Product |
abbrev |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 87 |
|
CategoryTheory.QuadrantProductTotal.degree |
abbrev |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 91 |
|
CategoryTheory.QuadrantProductTotal.horizontalIndex |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 95 |
|
CategoryTheory.QuadrantProductTotal.verticalIndex |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 99 |
|
CategoryTheory.QuadrantProductTotal.cycleIndex_horizontal |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 102 |
|
CategoryTheory.QuadrantProductTotal.cycleIndex_vertical |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 107 |
|
CategoryTheory.QuadrantProductTotal.horizontal |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 117 |
|
CategoryTheory.QuadrantProductTotal.vertical |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 123 |
|
CategoryTheory.QuadrantProductTotal.horizontalMap |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 130 |
|
CategoryTheory.QuadrantProductTotal.verticalMap |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 134 |
|
CategoryTheory.QuadrantProductTotal.horizontalMap_apply |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 137 |
|
CategoryTheory.QuadrantProductTotal.verticalMap_apply_zero |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 143 |
|
CategoryTheory.QuadrantProductTotal.verticalMap_apply_pos |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 148 |
|
CategoryTheory.QuadrantProductTotal.differential |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 156 |
|
CategoryTheory.QuadrantProductTotal.differential_eq |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 159 |
|
CategoryTheory.QuadrantProductTotal.differential_apply_zero |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 166 |
|
CategoryTheory.QuadrantProductTotal.differential_apply_pos |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 173 |
|
CategoryTheory.QuadrantProductTotal.horizontal_square |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 182 |
|
CategoryTheory.QuadrantProductTotal.vertical_square |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 196 |
|
CategoryTheory.QuadrantProductTotal.horizontal_vertical_comm |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 224 |
|
CategoryTheory.QuadrantProductTotal.differential_square |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 253 |
|
CategoryTheory.QuadrantProductTotal.productTotal |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 269 |
|
CategoryTheory.QuadrantProductTotal.mapDegree |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 297 |
|
CategoryTheory.QuadrantProductTotal.mapDegree_apply |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 301 |
|
CategoryTheory.QuadrantProductTotal.map_horizontal |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 306 |
|
CategoryTheory.QuadrantProductTotal.map_vertical |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 321 |
|
CategoryTheory.QuadrantProductTotal.map_differential |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 344 |
|
CategoryTheory.QuadrantProductTotal.productTotal_d |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 350 |
|
CategoryTheory.QuadrantProductTotal.nextHorizontalIndex |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 355 |
|
CategoryTheory.QuadrantProductTotal.nextVerticalIndex |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 359 |
|
CategoryTheory.QuadrantProductTotal.productTotal_d_apply_zero |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 363 |
|
CategoryTheory.QuadrantProductTotal.productTotal_d_apply_pos |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 373 |
|
CategoryTheory.QuadrantProductTotal.productTotalMap |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 386 |
|
CategoryTheory.QuadrantProductTotal.productTotalMap_f |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 400 |
|
CategoryTheory.QuadrantProductTotal.mapDegree_id |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 403 |
|
CategoryTheory.QuadrantProductTotal.mapDegree_comp |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 408 |
|
CategoryTheory.QuadrantProductTotal.productTotalMap_id |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 414 |
|
CategoryTheory.QuadrantProductTotal.productTotalMap_comp |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 421 |
|
CategoryTheory.QuadrantProductTotal.row_lift |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 431 |
|
CategoryTheory.QuadrantProductTotal.cycle_equation |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 457 |
|
CategoryTheory.QuadrantProductTotal.horizontal_at_zero |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 474 |
|
CategoryTheory.QuadrantProductTotal.first_kernel |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 482 |
|
CategoryTheory.QuadrantProductTotal.residual_kernel |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 503 |
|
CategoryTheory.QuadrantProductTotal.vertical_square_apply |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 520 |
|
CategoryTheory.QuadrantProductTotal.cycle_equation_step |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 529 |
|
CategoryTheory.QuadrantProductTotal.coordinate |
abbrev |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 541 |
|
CategoryTheory.QuadrantProductTotal.LiftState |
abbrev |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 548 |
|
CategoryTheory.QuadrantProductTotal.initialState_exists |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 555 |
|
CategoryTheory.QuadrantProductTotal.nextState_exists |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 570 |
|
CategoryTheory.QuadrantProductTotal.liftStates |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 606 |
|
CategoryTheory.QuadrantProductTotal.liftStates_first |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 613 |
|
CategoryTheory.QuadrantProductTotal.liftStates_step |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 620 |
|
CategoryTheory.QuadrantProductTotal.primitive |
def |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 633 |
|
CategoryTheory.QuadrantProductTotal.primitive_apply_index |
theorem |
HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 641 |
|