ComplexShapeSigns

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

Statistics

Metric	Count
Definitions Associative, TensorSigns, ε', instTensorSignsIntUp, instTensorSignsNatDown, instTotalComplexShape, instTotalComplexShapeSymmetryIntUp, r, symmetryEquiv, ε, ε₁, ε₂, π, ρ₁₂, ρ₂₃, σ, TotalComplexShape, symmSymmetry, ε₁, ε₂, π, TotalComplexShapeSymmetry, symmetry, σ, TotalComplexShapeSymmetrySymmetry	25
Theorems assoc, ε₁_eq_mul, ε₂_eq_mul, ε₂_ε₁, add_rel, rel_add, ε'_succ, add_rel, assoc, associative_ε₁_eq_mul, associative_ε₂_eq_mul, associative_ε₂_ε₁, instAssociative, next_add, next_add', next_π₁, next_π₂, prev_π₁, prev_π₂, rel_add, rel_π₁, rel_π₂, symmetryEquiv_apply_coe, symmetryEquiv_symm_apply_coe, ε_add, ε_down_ℕ, ε_succ, ε_up_ℤ, ε_zero, ε₁_def, ε₁_ε₂, ε₂_def, ε₂_ε₁, π_def, π_symm, σ_def, σ_symm, σ_ε₁, σ_ε₂, rel₁, rel₂, ε₂_ε₁, σ_ε₁, σ_ε₂, σ_symm	45
Total	70

ComplexShape

Definitions

Name	Category	Theorems
Associative 📖	CompData	1 math math: instAssociative
TensorSigns 📖	CompData	—
instTensorSignsIntUp 📖	CompOp	6 math math: CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂, σ_def, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, ε_up_ℤ
instTensorSignsNatDown 📖	CompOp	1 math math: ε_down_ℕ
instTotalComplexShape 📖	CompOp	11 math math: CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, ε₁_def, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂, instAssociative, HomologicalComplex.tensor_unit_d₂, σ_def, HomologicalComplex.unit_tensor_d₁, ε₂_def, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, π_def
instTotalComplexShapeSymmetryIntUp 📖	CompOp	1 math math: σ_def
r 📖	CompOp	—
symmetryEquiv 📖	CompOp	2 math math: symmetryEquiv_apply_coe, symmetryEquiv_symm_apply_coe
ε 📖	CompOp	6 math math: ε_succ, ε_add, ε_down_ℕ, ε_zero, ε₂_def, ε_up_ℤ
ε₁ 📖	CompOp	23 math math: associative_ε₂_ε₁, HomologicalComplex.mapBifunctor₂₃.d₂_eq, ε₁_ε₂, TotalComplexShapeSymmetry.σ_ε₁, HomologicalComplex₂.d₁_eq, Associative.ε₂_ε₁, HomologicalComplex₂.totalAux.d₁_eq, ε₂_ε₁, σ_ε₁, associative_ε₁_eq_mul, HomologicalComplex.mapBifunctor₂₃.d₁_eq, TotalComplexShapeSymmetry.σ_ε₂, σ_ε₂, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, Associative.ε₁_eq_mul, HomologicalComplex.mapBifunctor.d₁_eq', HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, HomologicalComplex₂.d₁_eq', HomologicalComplex.mapBifunctor₁₂.d₁_eq, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, HomologicalComplex.mapBifunctor₁₂.d₂_eq, HomologicalComplex₂.totalAux.d₁_eq', HomologicalComplex.mapBifunctor.d₁_eq
ε₂ 📖	CompOp	22 math math: associative_ε₂_ε₁, HomologicalComplex.mapBifunctor₂₃.d₂_eq, HomologicalComplex₂.totalAux.d₂_eq, HomologicalComplex.mapBifunctor₂₃.d₃_eq, ε₁_ε₂, TotalComplexShapeSymmetry.σ_ε₁, Associative.ε₂_ε₁, associative_ε₂_eq_mul, HomologicalComplex₂.totalAux.d₂_eq', HomologicalComplex.mapBifunctor.d₂_eq, ε₂_ε₁, σ_ε₁, TotalComplexShapeSymmetry.σ_ε₂, σ_ε₂, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, HomologicalComplex₂.d₂_eq, Associative.ε₂_eq_mul, HomologicalComplex.mapBifunctor.d₂_eq', HomologicalComplex₂.d₂_eq', HomologicalComplex.mapBifunctor₁₂.d₃_eq, HomologicalComplex.mapBifunctor₁₂.d₂_eq, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc
π 📖	CompOp	69 math math: HomologicalComplex₂.totalFlipIso_hom_f_D₁, associative_ε₂_ε₁, HomologicalComplex.mapBifunctor₂₃.d₂_eq, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, HomologicalComplex₂.d₁_eq_zero', HomologicalComplex₂.D₁_D₁_assoc, HomologicalComplex₂.total.mapAux.mapMap_D₁_assoc, HomologicalComplex.mapBifunctor₂₃.d₃_eq, HomologicalComplex₂.D₁_D₁, HomologicalComplex₂.D₂_D₁_assoc, HomologicalComplex₂.D₂_D₂, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ, HomologicalComplex₂.d₂_eq_zero, assoc, HomologicalComplex₂.total.mapAux.d₁_mapMap, Associative.ε₂_ε₁, HomologicalComplex₂.D₁_shape, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ, HomologicalComplex₂.totalFlipIsoX_hom_D₂_assoc, associative_ε₂_eq_mul, symmetryEquiv_apply_coe, symmetryEquiv_symm_apply_coe, HomologicalComplex₂.totalAux.d₂_eq', HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc, HomologicalComplex₂.d₁_eq_zero, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, Associative.assoc, π_symm, HomologicalComplex₂.total.mapAux.mapMap_D₁, associative_ε₁_eq_mul, HomologicalComplex₂.d₂_eq_zero', HomologicalComplex₂.total.mapAux.mapMap_D₂, HomologicalComplex₂.D₂_shape, HomologicalComplex₂.total.mapAux.mapMap_D₂_assoc, HomologicalComplex₂.totalFlipIso_hom_f_D₂, HomologicalComplex.mapBifunctor₂₃.d₁_eq, HomologicalComplex₂.D₁_totalShift₁XIso_hom, HomologicalComplex₂.D₂_totalShift₁XIso_hom, HomologicalComplex₂.totalFlipIso_hom_f_D₁_assoc, HomologicalComplex₂.totalFlipIsoX_hom_D₁, HomologicalComplex₂.D₂_D₂_assoc, HomologicalComplex₂.D₂_D₁, rel_π₂, HomologicalComplex₂.D₁_D₂_assoc, Associative.ε₂_eq_mul, rel_π₁, Associative.ε₁_eq_mul, HomologicalComplex₂.total.mapAux.d₂_mapMap, prev_π₁, next_π₁, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX, TotalComplexShapeSymmetry.symm, HomologicalComplex₂.total_d, HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc, HomologicalComplex₂.totalFlipIsoX_hom_D₂, HomologicalComplex₂.D₁_totalShift₂XIso_hom, HomologicalComplex.mapBifunctor₁₂.d₁_eq, HomologicalComplex₂.D₂_totalShift₂XIso_hom, HomologicalComplex.mapBifunctor₁₂.d₃_eq, HomologicalComplex.mapBifunctor₁₂.d₂_eq, HomologicalComplex₂.totalAux.d₁_eq', HomologicalComplex₂.D₁_D₂, HomologicalComplex₂.totalFlipIsoX_hom_D₁_assoc, next_π₂, HomologicalComplex₂.total.forget_map, HomologicalComplex₂.totalFlipIso_hom_f_D₂_assoc, prev_π₂
ρ₁₂ 📖	CompOp	—
ρ₂₃ 📖	CompOp	—
σ 📖	CompOp	12 math math: TotalComplexShapeSymmetrySymmetry.σ_symm, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc, σ_symm, HomologicalComplex.ι_mapBifunctorFlipIso_inv_assoc, σ_ε₁, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc, σ_ε₂, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom, HomologicalComplex.ι_mapBifunctorFlipIso_hom, HomologicalComplex.ι_mapBifunctorFlipIso_hom_assoc, HomologicalComplex.ι_mapBifunctorFlipIso_inv, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_rel 📖	mathematical	Rel	AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	TensorSigns.add_rel
assoc 📖	mathematical	—	π	—	Associative.assoc
associative_ε₁_eq_mul 📖	mathematical	—	ε₁ π Units Int.instMonoid Units.instMul	—	Associative.ε₁_eq_mul
associative_ε₂_eq_mul 📖	mathematical	—	ε₂ π Units Int.instMonoid Units.instMul	—	Associative.ε₂_eq_mul
associative_ε₂_ε₁ 📖	mathematical	—	Units Int.instMonoid Units.instMul ε₂ π ε₁	—	Associative.ε₂_ε₁
instAssociative 📖	mathematical	—	Associative instTotalComplexShape	—	add_assoc one_mul mul_one ε_add
next_add 📖	mathematical	Rel next	AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	next_eq' rel_add
next_add' 📖	mathematical	Rel next	AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	next_eq' add_rel
next_π₁ 📖	mathematical	Rel	next π	—	next_eq' rel_π₁
next_π₂ 📖	mathematical	Rel	next π	—	next_eq' rel_π₂
prev_π₁ 📖	mathematical	Rel	prev π	—	prev_eq' rel_π₁
prev_π₂ 📖	mathematical	Rel	prev π	—	prev_eq' rel_π₂
rel_add 📖	mathematical	Rel	AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	TensorSigns.rel_add
rel_π₁ 📖	mathematical	Rel	π	—	TotalComplexShape.rel₁
rel_π₂ 📖	mathematical	Rel	π	—	TotalComplexShape.rel₂
symmetryEquiv_apply_coe 📖	mathematical	—	Set Set.instMembership Set.preimage π Set.instSingletonSet DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike symmetryEquiv	—	—
symmetryEquiv_symm_apply_coe 📖	mathematical	—	Set Set.instMembership Set.preimage π Set.instSingletonSet DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm symmetryEquiv	—	—
ε_add 📖	mathematical	—	ε AddSemigroup.toAdd AddMonoid.toAddSemigroup Units Int.instMonoid Units.instMul	—	map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
ε_down_ℕ 📖	mathematical	—	ε Nat.instAddMonoid down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne instTensorSignsNatDown Units Int.instMonoid Int.instUnitsPow Nat.instCommSemiring AddCommMonoid.toNatModule Additive Additive.addCommMonoid CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
ε_succ 📖	mathematical	Rel	ε Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	TensorSigns.ε'_succ
ε_up_ℤ 📖	mathematical	—	ε Int.instAddMonoid up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instTensorSignsIntUp Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd
ε_zero 📖	mathematical	—	ε AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Units Int.instMonoid Units.instOne	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
ε₁_def 📖	mathematical	—	TotalComplexShape.ε₁ instTotalComplexShape Units Int.instMonoid Units.instOne	—	—
ε₁_ε₂ 📖	mathematical	Rel	Units Int.instMonoid Units.instMul ε₁ ε₂ Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	mul_one Int.units_mul_self mul_assoc ε₂_ε₁ neg_mul mul_neg one_mul
ε₂_def 📖	mathematical	—	TotalComplexShape.ε₂ instTotalComplexShape Units Int.instMonoid ε	—	—
ε₂_ε₁ 📖	mathematical	Rel	Units Int.instMonoid Units.instMul ε₂ ε₁ Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	TotalComplexShape.ε₂_ε₁
π_def 📖	mathematical	—	TotalComplexShape.π instTotalComplexShape AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	—
π_symm 📖	mathematical	—	π	—	TotalComplexShapeSymmetry.symm
σ_def 📖	mathematical	—	TotalComplexShapeSymmetry.σ up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instTotalComplexShape Int.instAddMonoid instTensorSignsIntUp instTotalComplexShapeSymmetryIntUp Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd
σ_symm 📖	mathematical	—	σ	—	TotalComplexShapeSymmetrySymmetry.σ_symm
σ_ε₁ 📖	mathematical	Rel	Units Int.instMonoid Units.instMul σ ε₁ ε₂	—	TotalComplexShapeSymmetry.σ_ε₁
σ_ε₂ 📖	mathematical	Rel	Units Int.instMonoid Units.instMul σ ε₂ ε₁	—	TotalComplexShapeSymmetry.σ_ε₂

ComplexShape.Associative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc 📖	mathematical	—	ComplexShape.π	—	—
ε₁_eq_mul 📖	mathematical	—	ComplexShape.ε₁ ComplexShape.π Units Int.instMonoid Units.instMul	—	—
ε₂_eq_mul 📖	mathematical	—	ComplexShape.ε₂ ComplexShape.π Units Int.instMonoid Units.instMul	—	—
ε₂_ε₁ 📖	mathematical	—	Units Int.instMonoid Units.instMul ComplexShape.ε₂ ComplexShape.π ComplexShape.ε₁	—	—

ComplexShape.TensorSigns

Definitions

Name	Category	Theorems
ε' 📖	CompOp	1 math math: ε'_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_rel 📖	mathematical	ComplexShape.Rel	AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	—
rel_add 📖	mathematical	ComplexShape.Rel	AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	—
ε'_succ 📖	mathematical	ComplexShape.Rel	DFunLike.coe MonoidHom Multiplicative Units Int.instMonoid MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Units.instMulOneClass MonoidHom.instFunLike ε' Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—

TotalComplexShape

Definitions

Name	Category	Theorems
symmSymmetry 📖	CompOp	—
ε₁ 📖	CompOp	2 math math: ComplexShape.ε₁_def, ε₂_ε₁
ε₂ 📖	CompOp	2 math math: ComplexShape.ε₂_def, ε₂_ε₁
π 📖	CompOp	3 math math: rel₂, rel₁, ComplexShape.π_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rel₁ 📖	mathematical	ComplexShape.Rel	π	—	—
rel₂ 📖	mathematical	ComplexShape.Rel	π	—	—
ε₂_ε₁ 📖	mathematical	ComplexShape.Rel	Units Int.instMonoid Units.instMul ε₂ ε₁ Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—

TotalComplexShapeSymmetry

Definitions

Name	Category	Theorems
symmetry 📖	CompOp	—
σ 📖	CompOp	3 math math: σ_ε₁, σ_ε₂, ComplexShape.σ_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
σ_ε₁ 📖	mathematical	ComplexShape.Rel	Units Int.instMonoid Units.instMul σ ComplexShape.ε₁ ComplexShape.ε₂	—	—
σ_ε₂ 📖	mathematical	ComplexShape.Rel	Units Int.instMonoid Units.instMul σ ComplexShape.ε₂ ComplexShape.ε₁	—	—

TotalComplexShapeSymmetrySymmetry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
σ_symm 📖	mathematical	—	ComplexShape.σ	—	—

(root)

Definitions

Name	Category	Theorems
TotalComplexShape 📖	CompData	—
TotalComplexShapeSymmetry 📖	CompData	—
TotalComplexShapeSymmetrySymmetry 📖	CompData	—

---

← Back to Index