Opposite

📁 Source: Mathlib/Algebra/Homology/Opposite.lean

Statistics

Metric	Count
Definitions cyclesOpIso, cyclesOpNatIso, homologyOp, homologyOpNatIso, homologyUnop, op, opCounitIso, opEquivalence, opFunctor, opInverse, opSymm, opUnitIso, opcyclesOpIso, opcyclesOpNatIso, unop, unopCounitIso, unopEquivalence, unopFunctor, unopInverse, unopSymm, unopUnitIso	21
Theorems op, unop, op, unop, acyclic_op_iff, cyclesOpIso_hom_naturality, cyclesOpIso_hom_naturality_assoc, cyclesOpIso_inv_naturality, cyclesOpIso_inv_naturality_assoc, cyclesOpNatIso_hom_app, cyclesOpNatIso_inv_app, exactAt_op_iff, fromOpcycles_op_cyclesOpIso_inv, fromOpcycles_op_cyclesOpIso_inv_assoc, homologyOp_hom_naturality, homologyOp_hom_naturality_assoc, instHasHomologyObjOppositeSymmUnopFunctorOp, instHasHomologyOppositeObjSymmOpFunctorOp, instHasHomologyOppositeOp, instHasHomologyUnopOfOpposite, instQuasiIsoAtMapOppositeSymmUnopFunctorOp, instQuasiIsoAtOppositeMapSymmOpFunctorOp, instQuasiIsoMapOppositeSymmUnopFunctorOp, instQuasiIsoOppositeMapSymmOpFunctorOp, opEquivalence_counitIso, opEquivalence_functor, opEquivalence_inverse, opEquivalence_unitIso, opFunctor_additive, opFunctor_map_f, opFunctor_obj, opInverse_map, opInverse_obj, opSymm_X, opSymm_d, op_X, op_d, opcyclesOpIso_hom_naturality, opcyclesOpIso_hom_naturality_assoc, opcyclesOpIso_hom_toCycles_op, opcyclesOpIso_hom_toCycles_op_assoc, opcyclesOpIso_inv_naturality, opcyclesOpIso_inv_naturality_assoc, quasiIsoAt_opFunctor_map_iff, quasiIsoAt_unopFunctor_map_iff, quasiIso_opFunctor_map_iff, quasiIso_unopFunctor_map_iff, unopEquivalence_counitIso, unopEquivalence_functor, unopEquivalence_inverse, unopEquivalence_unitIso, unopFunctor_additive, unopFunctor_map_f, unopFunctor_obj, unopInverse_map, unopInverse_obj, unopSymm_X, unopSymm_d, unop_X, unop_d, imageToKernel_op, imageToKernel_unop	62
Total	83

HomologicalComplex

Definitions

Name	Category	Theorems
cyclesOpIso 📖	CompOp	8 math math: cyclesOpIso_inv_naturality_assoc, cyclesOpNatIso_inv_app, fromOpcycles_op_cyclesOpIso_inv_assoc, cyclesOpIso_inv_naturality, cyclesOpIso_hom_naturality_assoc, cyclesOpIso_hom_naturality, cyclesOpNatIso_hom_app, fromOpcycles_op_cyclesOpIso_inv
cyclesOpNatIso 📖	CompOp	2 math math: cyclesOpNatIso_inv_app, cyclesOpNatIso_hom_app
homologyOp 📖	CompOp	2 math math: homologyOp_hom_naturality_assoc, homologyOp_hom_naturality
homologyOpNatIso 📖	CompOp	—
homologyUnop 📖	CompOp	—
op 📖	CompOp	34 math math: op_d, opcyclesOpIso_inv_naturality_assoc, instHasHomologyOppositeOp, extend_op_d_assoc, isStrictlySupportedOutside_op_iff, opcyclesOpIso_inv_naturality, extend.XOpIso_hom_d_op, extend.XOpIso_hom_d_op_assoc, opFunctor_obj, cyclesOpIso_inv_naturality_assoc, Acyclic.op, cyclesOpNatIso_inv_app, opcyclesOpIso_hom_naturality_assoc, opcyclesOpIso_hom_toCycles_op, opFunctor_map_f, isSupportedOutside_op_iff, exactAt_op_iff, fromOpcycles_op_cyclesOpIso_inv_assoc, homologyOp_hom_naturality_assoc, cyclesOpIso_inv_naturality, opcyclesOpIso_hom_naturality, extend_op_d, isStrictlySupported_op_iff, cyclesOpIso_hom_naturality_assoc, cyclesOpIso_hom_naturality, isSupported_op_iff, acyclic_op_iff, ExactAt.op, op_X, cyclesOpNatIso_hom_app, fromOpcycles_op_cyclesOpIso_inv, instIsStrictlySupportedOppositeOpOp, homologyOp_hom_naturality, opcyclesOpIso_hom_toCycles_op_assoc
opCounitIso 📖	CompOp	1 math math: opEquivalence_counitIso
opEquivalence 📖	CompOp	4 math math: opEquivalence_unitIso, opEquivalence_counitIso, opEquivalence_functor, opEquivalence_inverse
opFunctor 📖	CompOp	21 math math: opcyclesOpIso_inv_naturality_assoc, opcyclesOpIso_inv_naturality, opFunctor_obj, cyclesOpIso_inv_naturality_assoc, cyclesOpNatIso_inv_app, opcyclesOpIso_hom_naturality_assoc, opFunctor_map_f, instQuasiIsoAtOppositeMapSymmOpFunctorOp, homologyOp_hom_naturality_assoc, cyclesOpIso_inv_naturality, opcyclesOpIso_hom_naturality, instHasHomologyOppositeObjSymmOpFunctorOp, cyclesOpIso_hom_naturality_assoc, cyclesOpIso_hom_naturality, instQuasiIsoOppositeMapSymmOpFunctorOp, opEquivalence_functor, quasiIso_opFunctor_map_iff, cyclesOpNatIso_hom_app, opFunctor_additive, homologyOp_hom_naturality, quasiIsoAt_opFunctor_map_iff
opInverse 📖	CompOp	3 math math: opInverse_obj, opEquivalence_inverse, opInverse_map
opSymm 📖	CompOp	4 math math: opSymm_d, unopInverse_map, unopInverse_obj, opSymm_X
opUnitIso 📖	CompOp	1 math math: opEquivalence_unitIso
opcyclesOpIso 📖	CompOp	6 math math: opcyclesOpIso_inv_naturality_assoc, opcyclesOpIso_inv_naturality, opcyclesOpIso_hom_naturality_assoc, opcyclesOpIso_hom_toCycles_op, opcyclesOpIso_hom_naturality, opcyclesOpIso_hom_toCycles_op_assoc
opcyclesOpNatIso 📖	CompOp	—
unop 📖	CompOp	7 math math: unopFunctor_obj, unop_X, instHasHomologyUnopOfOpposite, unop_d, Acyclic.unop, unopFunctor_map_f, ExactAt.unop
unopCounitIso 📖	CompOp	1 math math: unopEquivalence_counitIso
unopEquivalence 📖	CompOp	4 math math: unopEquivalence_functor, unopEquivalence_unitIso, unopEquivalence_inverse, unopEquivalence_counitIso
unopFunctor 📖	CompOp	9 math math: unopFunctor_obj, unopEquivalence_functor, instQuasiIsoAtMapOppositeSymmUnopFunctorOp, instQuasiIsoMapOppositeSymmUnopFunctorOp, quasiIsoAt_unopFunctor_map_iff, quasiIso_unopFunctor_map_iff, unopFunctor_map_f, unopFunctor_additive, instHasHomologyObjOppositeSymmUnopFunctorOp
unopInverse 📖	CompOp	3 math math: unopInverse_map, unopInverse_obj, unopEquivalence_inverse
unopSymm 📖	CompOp	4 math math: unopSymm_X, opInverse_obj, unopSymm_d, opInverse_map
unopUnitIso 📖	CompOp	1 math math: unopEquivalence_unitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
acyclic_op_iff 📖	mathematical	—	Acyclic Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op	—	Acyclic.unop Acyclic.op
cyclesOpIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op instHasHomologyOppositeObjSymmOpFunctorOp instHasHomologyOppositeOp opcycles cyclesMap CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom op cyclesOpIso opcyclesMap	—	CategoryTheory.ShortComplex.cyclesOpIso_hom_naturality CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
cyclesOpIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite cycles CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op instHasHomologyOppositeObjSymmOpFunctorOp instHasHomologyOppositeOp cyclesMap CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver opcycles CategoryTheory.Iso.hom op cyclesOpIso opcyclesMap	—	instHasHomologyOppositeObjSymmOpFunctorOp instHasHomologyOppositeOp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesOpIso_hom_naturality
cyclesOpIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op opcycles cycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op instHasHomologyOppositeOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver opcyclesMap CategoryTheory.Iso.inv cyclesOpIso CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor instHasHomologyOppositeObjSymmOpFunctorOp cyclesMap CategoryTheory.Functor.map	—	CategoryTheory.ShortComplex.cyclesOpIso_inv_naturality CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
cyclesOpIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op opcycles Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver opcyclesMap cycles CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op instHasHomologyOppositeOp CategoryTheory.Iso.inv cyclesOpIso cyclesMap CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor CategoryTheory.Functor.map instHasHomologyOppositeObjSymmOpFunctorOp	—	instHasHomologyOppositeOp instHasHomologyOppositeObjSymmOpFunctorOp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesOpIso_inv_naturality
cyclesOpNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite HomologicalComplex CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.comp CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm opFunctor cyclesFunctor CategoryTheory.ShortComplex.instCategoryWithHomologyOpposite CategoryTheory.Functor.op opcyclesFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category cyclesOpNatIso cycles op Opposite.unop Opposite.op opcycles cyclesOpIso	—	CategoryTheory.ShortComplex.instCategoryWithHomologyOpposite
cyclesOpNatIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite HomologicalComplex CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.op opcyclesFunctor CategoryTheory.Functor.comp CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm opFunctor cyclesFunctor CategoryTheory.ShortComplex.instCategoryWithHomologyOpposite CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category cyclesOpNatIso cycles op Opposite.unop Opposite.op opcycles cyclesOpIso	—	CategoryTheory.ShortComplex.instCategoryWithHomologyOpposite
exactAt_op_iff 📖	mathematical	—	ExactAt Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op	—	ExactAt.unop ExactAt.op
fromOpcycles_op_cyclesOpIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op X opcycles cycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op instHasHomologyOppositeOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver fromOpcycles CategoryTheory.Iso.inv cyclesOpIso toCycles	—	instHasHomologyOppositeOp CategoryTheory.ShortComplex.fromOpcycles_op_cyclesOpIso_inv CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology ComplexShape.next_eq' toCycles_eq_zero fromOpcycles_eq_zero CategoryTheory.Limits.op_zero CategoryTheory.Limits.zero_comp
fromOpcycles_op_cyclesOpIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op X opcycles Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver fromOpcycles cycles CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op instHasHomologyOppositeOp CategoryTheory.Iso.inv cyclesOpIso toCycles	—	instHasHomologyOppositeOp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromOpcycles_op_cyclesOpIso_inv
homologyOp_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op instHasHomologyOppositeObjSymmOpFunctorOp instHasHomologyOppositeOp homologyMap CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom op homologyOp	—	CategoryTheory.ShortComplex.homologyOpIso_hom_naturality
homologyOp_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite homology CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op instHasHomologyOppositeObjSymmOpFunctorOp instHasHomologyOppositeOp homologyMap CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom op homologyOp	—	instHasHomologyOppositeObjSymmOpFunctorOp instHasHomologyOppositeOp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyOp_hom_naturality
instHasHomologyObjOppositeSymmUnopFunctorOp 📖	mathematical	—	HasHomology ComplexShape.symm CategoryTheory.Functor.obj Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite instCategory unopFunctor Opposite.op	—	instHasHomologyUnopOfOpposite
instHasHomologyOppositeObjSymmOpFunctorOp 📖	mathematical	—	HasHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op	—	instHasHomologyOppositeOp
instHasHomologyOppositeOp 📖	mathematical	—	HasHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op	—	CategoryTheory.ShortComplex.instHasHomologyOppositeOp
instHasHomologyUnopOfOpposite 📖	mathematical	—	HasHomology ComplexShape.symm unop	—	CategoryTheory.ShortComplex.instHasHomologyUnopOfOpposite
instQuasiIsoAtMapOppositeSymmUnopFunctorOp 📖	mathematical	—	QuasiIsoAt ComplexShape.symm CategoryTheory.Functor.obj Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite instCategory unopFunctor Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instHasHomologyObjOppositeSymmUnopFunctorOp	—	instHasHomologyObjOppositeSymmUnopFunctorOp quasiIsoAt_unopFunctor_map_iff
instQuasiIsoAtOppositeMapSymmOpFunctorOp 📖	mathematical	—	QuasiIsoAt Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instHasHomologyOppositeObjSymmOpFunctorOp	—	instHasHomologyOppositeObjSymmOpFunctorOp quasiIsoAt_opFunctor_map_iff
instQuasiIsoMapOppositeSymmUnopFunctorOp 📖	mathematical	HasHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	QuasiIso ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory unopFunctor Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instHasHomologyObjOppositeSymmUnopFunctorOp	—	instHasHomologyObjOppositeSymmUnopFunctorOp quasiIso_unopFunctor_map_iff
instQuasiIsoOppositeMapSymmOpFunctorOp 📖	mathematical	HasHomology	QuasiIso Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instHasHomologyOppositeObjSymmOpFunctorOp	—	instHasHomologyOppositeObjSymmOpFunctorOp quasiIso_opFunctor_map_iff
opEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory opEquivalence opCounitIso	—	—
opEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory opEquivalence opFunctor	—	—
opEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory opEquivalence opInverse	—	—
opEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory opEquivalence opUnitIso	—	—
opFunctor_additive 📖	mathematical	—	CategoryTheory.Functor.Additive Opposite HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory CategoryTheory.instPreadditiveOpposite instPreadditive opFunctor	—	—
opFunctor_map_f 📖	mathematical	—	Hom.f Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op Opposite.unop HomologicalComplex CategoryTheory.Functor.map instCategory opFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X Quiver.Hom.unop	—	—
opFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite HomologicalComplex CategoryTheory.Category.opposite instCategory CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm opFunctor op Opposite.unop	—	—
opInverse_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory opInverse Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unopSymm Quiver.Hom.unop X Hom.f	—	—
opInverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory opInverse Opposite.op unopSymm	—	—
opSymm_X 📖	mathematical	—	X Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite opSymm Opposite.op ComplexShape.symm	—	—
opSymm_d 📖	mathematical	—	d Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite opSymm Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X ComplexShape.symm	—	—
op_X 📖	mathematical	—	X Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op Opposite.op	—	—
op_d 📖	mathematical	—	d Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X	—	—
opcyclesOpIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op instHasHomologyOppositeObjSymmOpFunctorOp instHasHomologyOppositeOp cycles opcyclesMap CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom op opcyclesOpIso cyclesMap	—	CategoryTheory.ShortComplex.opcyclesOpIso_hom_naturality CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
opcyclesOpIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite opcycles CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op instHasHomologyOppositeObjSymmOpFunctorOp instHasHomologyOppositeOp opcyclesMap CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver cycles CategoryTheory.Iso.hom op opcyclesOpIso cyclesMap	—	instHasHomologyOppositeObjSymmOpFunctorOp instHasHomologyOppositeOp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesOpIso_hom_naturality
opcyclesOpIso_hom_toCycles_op 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op instHasHomologyOppositeOp Opposite.op cycles X CategoryTheory.Iso.hom opcyclesOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver toCycles fromOpcycles	—	instHasHomologyOppositeOp CategoryTheory.ShortComplex.opcyclesOpIso_hom_toCycles_op CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology ComplexShape.prev_eq' toCycles_eq_zero fromOpcycles_eq_zero CategoryTheory.Limits.op_zero CategoryTheory.Limits.comp_zero
opcyclesOpIso_hom_toCycles_op_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite opcycles CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op instHasHomologyOppositeOp Opposite.op cycles CategoryTheory.Iso.hom opcyclesOpIso X Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver toCycles fromOpcycles	—	instHasHomologyOppositeOp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesOpIso_hom_toCycles_op
opcyclesOpIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op cycles opcycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op instHasHomologyOppositeOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver cyclesMap CategoryTheory.Iso.inv opcyclesOpIso CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor instHasHomologyOppositeObjSymmOpFunctorOp opcyclesMap CategoryTheory.Functor.map	—	CategoryTheory.ShortComplex.opcyclesOpIso_inv_naturality CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
opcyclesOpIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op cycles Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver cyclesMap opcycles CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm op instHasHomologyOppositeOp CategoryTheory.Iso.inv opcyclesOpIso opcyclesMap CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor CategoryTheory.Functor.map instHasHomologyOppositeObjSymmOpFunctorOp	—	instHasHomologyOppositeOp instHasHomologyOppositeObjSymmOpFunctorOp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesOpIso_inv_naturality
quasiIsoAt_opFunctor_map_iff 📖	mathematical	—	QuasiIsoAt Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instHasHomologyOppositeObjSymmOpFunctorOp	—	instHasHomologyOppositeObjSymmOpFunctorOp CategoryTheory.ShortComplex.quasiIso_opMap_iff
quasiIsoAt_unopFunctor_map_iff 📖	mathematical	—	QuasiIsoAt ComplexShape.symm CategoryTheory.Functor.obj Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite instCategory unopFunctor Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instHasHomologyObjOppositeSymmUnopFunctorOp	—	instHasHomologyObjOppositeSymmUnopFunctorOp instHasHomologyOppositeObjSymmOpFunctorOp quasiIsoAt_opFunctor_map_iff
quasiIso_opFunctor_map_iff 📖	mathematical	HasHomology	QuasiIso Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory opFunctor Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instHasHomologyOppositeObjSymmOpFunctorOp	—	instHasHomologyOppositeObjSymmOpFunctorOp
quasiIso_unopFunctor_map_iff 📖	mathematical	HasHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	QuasiIso ComplexShape.symm CategoryTheory.Functor.obj HomologicalComplex instCategory unopFunctor Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instHasHomologyObjOppositeSymmUnopFunctorOp	—	instHasHomologyObjOppositeSymmUnopFunctorOp
unopEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory unopEquivalence unopCounitIso	—	—
unopEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory unopEquivalence unopFunctor	—	—
unopEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory unopEquivalence unopInverse	—	—
unopEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm instCategory unopEquivalence unopUnitIso	—	—
unopFunctor_additive 📖	mathematical	—	CategoryTheory.Functor.Additive Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.symm instCategory CategoryTheory.instPreadditiveOpposite instPreadditive unopFunctor	—	—
unopFunctor_map_f 📖	mathematical	—	Hom.f ComplexShape.symm unop Opposite.unop HomologicalComplex Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.Functor.map instCategory unopFunctor Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X	—	—
unopFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite HomologicalComplex CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite instCategory ComplexShape.symm unopFunctor unop Opposite.unop	—	—
unopInverse_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex ComplexShape.symm instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite unopInverse Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct opSymm X Hom.f	—	—
unopInverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex ComplexShape.symm instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite unopInverse Opposite.op opSymm	—	—
unopSymm_X 📖	mathematical	—	X unopSymm Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm	—	—
unopSymm_d 📖	mathematical	—	d unopSymm Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm	—	—
unop_X 📖	mathematical	—	X ComplexShape.symm unop Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	—	—
unop_d 📖	mathematical	—	d ComplexShape.symm unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	—	—

HomologicalComplex.Acyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	HomologicalComplex.Acyclic	Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm HomologicalComplex.op	—	HomologicalComplex.ExactAt.op
unop 📖	mathematical	HomologicalComplex.Acyclic Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	ComplexShape.symm HomologicalComplex.unop	—	HomologicalComplex.ExactAt.unop

HomologicalComplex.ExactAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	HomologicalComplex.ExactAt	Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm HomologicalComplex.op	—	CategoryTheory.ShortComplex.Exact.op
unop 📖	mathematical	HomologicalComplex.ExactAt Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	ComplexShape.symm HomologicalComplex.unop	—	CategoryTheory.ShortComplex.Exact.unop

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
imageToKernel_op 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	imageToKernel Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite Opposite.op Quiver.Hom.op CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.instAbelianOpposite CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.image CategoryTheory.Limits.kernelSubobject CategoryTheory.Iso.hom CategoryTheory.Iso.trans CategoryTheory.Limits.imageSubobjectIso CategoryTheory.Iso.symm CategoryTheory.imageOpOp CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.desc CategoryTheory.Limits.factorThruImage CategoryTheory.Iso.inv CategoryTheory.Limits.kernel CategoryTheory.Limits.kernelSubobjectIso CategoryTheory.kernelOpOp	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels imageToKernel_arrow CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage CategoryTheory.Category.assoc CategoryTheory.Limits.kernelSubobject_arrow' CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.cokernel.π_desc
imageToKernel_unop 📖	mathematical	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	imageToKernel Opposite.unop Quiver.Hom.unop CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.image CategoryTheory.instAbelianOpposite CategoryTheory.Limits.kernelSubobject CategoryTheory.Iso.hom CategoryTheory.Iso.trans CategoryTheory.Limits.imageSubobjectIso CategoryTheory.Iso.symm CategoryTheory.imageUnopUnop CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.desc CategoryTheory.Limits.factorThruImage CategoryTheory.Iso.inv CategoryTheory.Limits.kernel CategoryTheory.Limits.kernelSubobjectIso CategoryTheory.kernelUnopUnop	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels imageToKernel_arrow CategoryTheory.Category.assoc CategoryTheory.Limits.kernelSubobject_arrow' CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.cokernel.π_desc CategoryTheory.factorThruImage_comp_imageUnopOp_inv CategoryTheory.Limits.imageSubobject_arrow

---

← Back to Index