Extend

📁 Source: Mathlib/Algebra/Homology/Embedding/Extend.lean

Statistics

Metric	Count
Definitions extendFunctor, fullyFaithfulExtendFunctor, extend, X, XIso, XOpIso, d, mapX, extendMap, extendOpIso, extendSingleIso, extendXIso	12
Theorems extendFunctor_map, extendFunctor_obj, instAdditiveHomologicalComplexExtendFunctor, instFaithfulHomologicalComplexExtendFunctor, instFullHomologicalComplexExtendFunctor, instPreservesZeroMorphismsHomologicalComplexExtendFunctor, XOpIso_hom_d_op, XOpIso_hom_d_op_assoc, d_eq, d_none_eq_zero, d_none_eq_zero', isZero_X, mapX_none, mapX_some, extendMap_add, extendMap_comp, extendMap_comp_assoc, extendMap_f, extendMap_f_eq_zero, extendMap_id, extendMap_id_f, extendMap_zero, extendSingleIso_hom_f, extendSingleIso_hom_f_assoc, extendSingleIso_inv_f, extendSingleIso_inv_f_assoc, extend_d_eq, extend_d_from_eq_zero, extend_d_to_eq_zero, extend_op_d, extend_op_d_assoc, extend_single_d, instIsStrictlySupportedExtend, isZero_extend_X, isZero_extend_X'	35
Total	47

ComplexShape.Embedding

Definitions

Name	Category	Theorems
extendFunctor 📖	CompOp	6 math math: instFaithfulHomologicalComplexExtendFunctor, extendFunctor_map, instFullHomologicalComplexExtendFunctor, instPreservesZeroMorphismsHomologicalComplexExtendFunctor, instAdditiveHomologicalComplexExtendFunctor, extendFunctor_obj
fullyFaithfulExtendFunctor 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex HomologicalComplex.instCategory extendFunctor HomologicalComplex.extendMap	—	—
extendFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory extendFunctor HomologicalComplex.extend	—	—
instAdditiveHomologicalComplexExtendFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex.instPreadditive extendFunctor	—	HomologicalComplex.extendMap_add
instFaithfulHomologicalComplexExtendFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful HomologicalComplex HomologicalComplex.instCategory extendFunctor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullHomologicalComplexExtendFunctor 📖	mathematical	—	CategoryTheory.Functor.Full HomologicalComplex HomologicalComplex.instCategory extendFunctor	—	CategoryTheory.Functor.FullyFaithful.full
instPreservesZeroMorphismsHomologicalComplexExtendFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms extendFunctor	—	HomologicalComplex.extendMap_zero

HomologicalComplex

Definitions

Name	Category	Theorems
extend 📖	CompOp	97 math math: extendSingleIso_inv_f, extend_exactAt, ComplexShape.Embedding.isIso_liftExtend_f_iff, homologyπ_extendHomologyIso_hom, quasiIso_extendMap_iff, extend.leftHomologyData_π, extend.d_comp_eq_zero_iff, extend.homologyData_left, extend_exactAt_iff, extend.homologyData'_left_H, extendHomologyIso_hom_naturality, ComplexShape.Embedding.liftExtend.comm_assoc, extendHomologyIso_hom_naturality_assoc, quasiIsoAt_extendMap_iff, extend_op_d_assoc, Homotopy.extend_hom_eq, extendSingleIso_inv_f_assoc, extendHomologyIso_hom_homologyι_assoc, CochainComplex.instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat, homologyπ_extendHomologyIso_inv, extendCyclesIso_inv_iCycles_assoc, extendMap_f, extendSingleIso_hom_f_assoc, extendMap_comp_assoc, extendCyclesIso_hom_naturality_assoc, ComplexShape.Embedding.homRestrict_precomp, Homotopy.extend.hom_eq_zero₁, ComplexShape.Embedding.epi_liftExtend_f_iff, extend_single_d, extend.hasHomology, extend_d_to_eq_zero, isZero_extend_X, extend.rightHomologyData.d_comp_desc_eq_zero_iff, ComplexShape.Embedding.homRestrict_comp_extendMap_assoc, extend.homologyData'_right_H, homologyπ_extendHomologyIso_inv_assoc, extend_op_d, ComplexShape.Embedding.mono_liftExtend_f_iff, extend.rightHomologyData_p, extend.leftHomologyData_H, extend.homologyData'_iso, instQuasiIsoExtendMap, ComplexShape.Embedding.liftExtend.comm, Homotopy.ofExtend_hom, extend.rightHomologyData_g', extend.rightHomologyData_ι, extend.homologyData'_right_p, extendCyclesIso_hom_iCycles, extend.homologyData'_left_i, ComplexShape.Embedding.homEquiv_symm_apply, ComplexShape.Embedding.homEquiv_apply_coe, pOpcycles_extendOpcyclesIso_hom_assoc, pOpcycles_extendOpcyclesIso_inv, homologyπ_extendHomologyIso_hom_assoc, extendMap_add, isZero_extend_X', extend_d_from_eq_zero, Homotopy.extend.hom_eq_zero₂, extend.rightHomologyData_H, extend.homologyData'_right_ι, ComplexShape.Embedding.liftExtend_f, extendCyclesIso_hom_naturality, extend.leftHomologyData_i, extend.comp_d_eq_zero_iff, ComplexShape.Embedding.liftExtend.f_eq, extend.instHasHomologyF, extend.instHasHomology, instIsStrictlySupportedExtend, ComplexShape.Embedding.homRestrict_precomp_assoc, extend.homologyData'_right_Q, CochainComplex.instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat, extend.leftHomologyData_K, pOpcycles_extendOpcyclesIso_hom, extendCyclesIso_inv_iCycles, extendCyclesIso_hom_iCycles_assoc, ComplexShape.Embedding.homRestrict_f, extend_d_eq, extendMap_comp, extend.homologyData'_left_π, ComplexShape.Embedding.homRestrict.f_eq, extendHomologyIso_inv_homologyι, extend.homologyData'_left_K, extend.homologyData_iso, extend.leftHomologyData.lift_d_comp_eq_zero_iff, extendMap_zero, extendMap_f_eq_zero, ComplexShape.Embedding.extendFunctor_obj, Homotopy.extend.hom_eq, extendHomologyIso_inv_homologyι_assoc, pOpcycles_extendOpcyclesIso_inv_assoc, extend.homologyData_right, extendSingleIso_hom_f, ComplexShape.Embedding.homRestrict_comp_extendMap, extend.rightHomologyData_Q, extendMap_id, extendHomologyIso_hom_homologyι, extendMap_id_f
extendMap 📖	CompOp	20 math math: quasiIso_extendMap_iff, extendHomologyIso_hom_naturality, extendHomologyIso_hom_naturality_assoc, quasiIsoAt_extendMap_iff, Homotopy.extend_hom_eq, extendMap_f, extendMap_comp_assoc, extendCyclesIso_hom_naturality_assoc, ComplexShape.Embedding.extendFunctor_map, ComplexShape.Embedding.homRestrict_comp_extendMap_assoc, instQuasiIsoExtendMap, Homotopy.ofExtend_hom, extendMap_add, extendCyclesIso_hom_naturality, extendMap_comp, extendMap_zero, extendMap_f_eq_zero, ComplexShape.Embedding.homRestrict_comp_extendMap, extendMap_id, extendMap_id_f
extendOpIso 📖	CompOp	2 math math: extend_op_d_assoc, extend_op_d
extendSingleIso 📖	CompOp	4 math math: extendSingleIso_inv_f, extendSingleIso_inv_f_assoc, extendSingleIso_hom_f_assoc, extendSingleIso_hom_f
extendXIso 📖	CompOp	28 math math: extendSingleIso_inv_f, extend.d_comp_eq_zero_iff, Homotopy.extend_hom_eq, extendSingleIso_inv_f_assoc, extendCyclesIso_inv_iCycles_assoc, extendMap_f, extendSingleIso_hom_f_assoc, extend.rightHomologyData_p, Homotopy.ofExtend_hom, extend.rightHomologyData_g', extend.homologyData'_right_p, extendCyclesIso_hom_iCycles, extend.homologyData'_left_i, pOpcycles_extendOpcyclesIso_hom_assoc, pOpcycles_extendOpcyclesIso_inv, ComplexShape.Embedding.liftExtend_f, extend.leftHomologyData_i, extend.comp_d_eq_zero_iff, ComplexShape.Embedding.liftExtend.f_eq, pOpcycles_extendOpcyclesIso_hom, extendCyclesIso_inv_iCycles, extendCyclesIso_hom_iCycles_assoc, ComplexShape.Embedding.homRestrict_f, extend_d_eq, ComplexShape.Embedding.homRestrict.f_eq, Homotopy.extend.hom_eq, pOpcycles_extendOpcyclesIso_inv_assoc, extendSingleIso_hom_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendMap_add 📖	mathematical	—	extendMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom extend	—	hom_ext extendMap_f CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.comp_add CategoryTheory.Limits.IsZero.eq_of_src isZero_extend_X
extendMap_comp 📖	mathematical	—	extendMap CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory extend	—	hom_ext extendMap_f CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc extendMap_f_eq_zero CategoryTheory.Limits.comp_zero
extendMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory extend extendMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendMap_comp
extendMap_f 📖	mathematical	ComplexShape.Embedding.f	Hom.f extend extendMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom extendXIso CategoryTheory.Iso.inv	—	ComplexShape.Embedding.r_eq_some extend.mapX_some
extendMap_f_eq_zero 📖	mathematical	—	Hom.f extend extendMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	extend.mapX_none ComplexShape.Embedding.r_eq_none
extendMap_id 📖	mathematical	—	extendMap CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory extend	—	hom_ext extendMap_id_f
extendMap_id_f 📖	mathematical	—	Hom.f extend extendMap CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory X	—	extendMap_f CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Limits.IsZero.eq_of_src isZero_extend_X
extendMap_zero 📖	mathematical	—	extendMap Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom extend	—	hom_ext extendMap_f CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero CategoryTheory.Limits.IsZero.eq_of_src isZero_extend_X
extendSingleIso_hom_f 📖	mathematical	ComplexShape.Embedding.f	Hom.f extend CategoryTheory.Functor.obj HomologicalComplex instCategory single CategoryTheory.Iso.hom extendSingleIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X extendXIso singleObjXSelf CategoryTheory.Iso.inv	—	mkHomToSingle_f CategoryTheory.Category.assoc
extendSingleIso_hom_f_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X extend CategoryTheory.Functor.obj HomologicalComplex instCategory single Hom.f CategoryTheory.Iso.hom extendSingleIso extendXIso singleObjXSelf CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendSingleIso_hom_f
extendSingleIso_inv_f 📖	mathematical	ComplexShape.Embedding.f	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory single extend CategoryTheory.Iso.inv extendSingleIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom singleObjXSelf extendXIso	—	mkHomFromSingle_f
extendSingleIso_inv_f_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Functor.obj HomologicalComplex instCategory single extend Hom.f CategoryTheory.Iso.inv extendSingleIso CategoryTheory.Iso.hom singleObjXSelf extendXIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendSingleIso_inv_f
extend_d_eq 📖	mathematical	ComplexShape.Embedding.f	d extend CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom extendXIso CategoryTheory.Iso.inv	—	extend.d_eq ComplexShape.Embedding.r_eq_some
extend_d_from_eq_zero 📖	mathematical	ComplexShape.Embedding.f ComplexShape.Rel ComplexShape.next	d extend Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	extend.d_none_eq_zero' ComplexShape.Embedding.f_eq_of_r_eq_some extend_d_eq shape ComplexShape.next_eq' CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
extend_d_to_eq_zero 📖	mathematical	ComplexShape.Embedding.f ComplexShape.Rel ComplexShape.prev	d extend Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	extend.d_none_eq_zero ComplexShape.Embedding.f_eq_of_r_eq_some extend_d_eq shape ComplexShape.prev_eq' CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
extend_op_d 📖	mathematical	—	d Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm extend CategoryTheory.Limits.hasZeroObject_op op ComplexShape.Embedding.op CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct X Hom.f CategoryTheory.Iso.hom HomologicalComplex instCategory extendOpIso Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv	—	CategoryTheory.Limits.hasZeroObject_op Hom.comm comp_f_assoc CategoryTheory.Iso.hom_inv_id id_f CategoryTheory.Category.id_comp
extend_op_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite X CategoryTheory.Limits.hasZeroMorphismsOpposite ComplexShape.symm extend CategoryTheory.Limits.hasZeroObject_op op ComplexShape.Embedding.op d Hom.f CategoryTheory.Iso.hom HomologicalComplex instCategory extendOpIso Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv	—	CategoryTheory.Limits.hasZeroObject_op CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extend_op_d
extend_single_d 📖	mathematical	—	d extend CategoryTheory.Functor.obj HomologicalComplex instCategory single Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	extend_d_eq CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero CategoryTheory.Limits.IsZero.eq_of_tgt isZero_extend_X CategoryTheory.Limits.IsZero.eq_of_src
instIsStrictlySupportedExtend 📖	mathematical	—	IsStrictlySupported extend	—	isZero_extend_X
isZero_extend_X 📖	mathematical	—	CategoryTheory.Limits.IsZero X extend	—	isZero_extend_X' ComplexShape.Embedding.r_eq_none
isZero_extend_X' 📖	mathematical	ComplexShape.Embedding.r	CategoryTheory.Limits.IsZero X extend	—	extend.isZero_X

HomologicalComplex.extend

Definitions

Name	Category	Theorems
X 📖	CompOp	9 math math: d_none_eq_zero', XOpIso_hom_d_op, XOpIso_hom_d_op_assoc, d_none_eq_zero, mapX_some, isZero_X, Homotopy.extend.homAux_eq, d_eq, mapX_none
XIso 📖	CompOp	3 math math: mapX_some, Homotopy.extend.homAux_eq, d_eq
XOpIso 📖	CompOp	2 math math: XOpIso_hom_d_op, XOpIso_hom_d_op_assoc
d 📖	CompOp	5 math math: d_none_eq_zero', XOpIso_hom_d_op, XOpIso_hom_d_op_assoc, d_none_eq_zero, d_eq
mapX 📖	CompOp	2 math math: mapX_some, mapX_none

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
XOpIso_hom_d_op 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct X ComplexShape.symm CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroObject_op CategoryTheory.Limits.hasZeroMorphismsOpposite HomologicalComplex.op Opposite.op CategoryTheory.Iso.hom XOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver d	—	CategoryTheory.Limits.hasZeroObject_op d_none_eq_zero' CategoryTheory.Limits.comp_zero d_none_eq_zero CategoryTheory.Limits.zero_comp d_eq CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
XOpIso_hom_d_op_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite X ComplexShape.symm CategoryTheory.Limits.hasZeroObject_op CategoryTheory.Limits.hasZeroMorphismsOpposite HomologicalComplex.op Opposite.op CategoryTheory.Iso.hom XOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver d	—	CategoryTheory.Limits.hasZeroObject_op CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XOpIso_hom_d_op
d_eq 📖	mathematical	—	d CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X CategoryTheory.Iso.hom XIso HomologicalComplex.d CategoryTheory.Iso.inv	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
d_none_eq_zero 📖	mathematical	—	d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
d_none_eq_zero' 📖	mathematical	—	d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
isZero_X 📖	mathematical	—	CategoryTheory.Limits.IsZero X	—	CategoryTheory.Limits.isZero_zero
mapX_none 📖	mathematical	—	mapX Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
mapX_some 📖	mathematical	—	mapX CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X CategoryTheory.Iso.hom XIso HomologicalComplex.Hom.f CategoryTheory.Iso.inv	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id

---

← Back to Index