Loogle!
Result
Found 122 definitions mentioning Units, Int, Int.instMonoid and HSMul.hSMul. Of these, 122 match your pattern(s).
- ZMod.smul_units_def 📋 Mathlib.Data.ZMod.IntUnitsPower
(z : ZMod 2) (au : Additive ℤˣ) : z • au = z.val • au - ZMod.natCast_smul_units 📋 Mathlib.Data.ZMod.IntUnitsPower
(n : ℕ) (au : Additive ℤˣ) : ↑n • au = n • au - ofMul_uzpow 📋 Mathlib.Data.ZMod.IntUnitsPower
{R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (u : ℤˣ) (r : R) : Additive.ofMul (u ^ r) = r • Additive.ofMul u - toMul_uzpow 📋 Mathlib.Data.ZMod.IntUnitsPower
{R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (u : Additive ℤˣ) (r : R) : Additive.toMul (r • u) = Additive.toMul u ^ r - AlternatingMap.map_congr_perm 📋 Mathlib.LinearAlgebra.Alternating.Basic
{R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') (v : ι → M) [DecidableEq ι] [Fintype ι] (σ : Equiv.Perm ι) : g v = Equiv.Perm.sign σ • g (v ∘ ⇑σ) - AlternatingMap.map_perm 📋 Mathlib.LinearAlgebra.Alternating.Basic
{R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') [DecidableEq ι] [Fintype ι] (v : ι → M) (σ : Equiv.Perm ι) : g (v ∘ ⇑σ) = Equiv.Perm.sign σ • g v - AlternatingMap.domDomCongr_perm 📋 Mathlib.LinearAlgebra.Alternating.Basic
{R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) : AlternatingMap.domDomCongr σ g = Equiv.Perm.sign σ • g - MultilinearMap.alternatization_apply 📋 Mathlib.LinearAlgebra.Alternating.Basic
{R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (m : MultilinearMap R (fun x => M) N') (v : ι → M) : (MultilinearMap.alternatization m) v = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • (MultilinearMap.domDomCongr σ m) v - MultilinearMap.alternatization_coe 📋 Mathlib.LinearAlgebra.Alternating.Basic
{R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (m : MultilinearMap R (fun x => M) N') : ↑(MultilinearMap.alternatization m) = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m - MultilinearMap.alternatization_def 📋 Mathlib.LinearAlgebra.Alternating.Basic
{R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (m : MultilinearMap R (fun x => M) N') : ⇑(MultilinearMap.alternatization m) = ⇑(∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m) - Matrix.det_neg_eq_smul 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Basic
{n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) : (-A).det = (-1) ^ Fintype.card n • A.det - Matrix.det_apply 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Basic
{n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (M : Matrix n n R) : M.det = ∑ σ : Equiv.Perm n, Equiv.Perm.sign σ • ∏ i : n, M (σ i) i - CategoryTheory.Preadditive.smul_iso_hom 📋 Mathlib.CategoryTheory.Preadditive.Basic
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} (a : ℤˣ) (e : X ≅ Y) : (a • e).hom = a • e.hom - CategoryTheory.Preadditive.smul_iso_inv 📋 Mathlib.CategoryTheory.Preadditive.Basic
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} (a : ℤˣ) (e : X ≅ Y) : (a • e).inv = a⁻¹ • e.inv - CategoryTheory.NatTrans.app_units_zsmul 📋 Mathlib.CategoryTheory.Preadditive.FunctorCategory
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {F G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (n : ℤˣ) : (n • α).app X = n • α.app X - HomologicalComplex₂.d₂_eq' 📋 Mathlib.Algebra.Homology.TotalComplex
{C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotalOrZero c₁₂ i₁ i₂' i₁₂) - HomologicalComplex₂.d₂_eq 📋 Mathlib.Algebra.Homology.TotalComplex
{C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotal c₁₂ i₁ i₂' i₁₂ h') - HomologicalComplex₂.d₁_eq' 📋 Mathlib.Algebra.Homology.TotalComplex
{C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotalOrZero c₁₂ i₁' i₂ i₁₂) - HomologicalComplex₂.totalAux.d₂_eq' 📋 Mathlib.Algebra.Homology.TotalComplex
{C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂) - HomologicalComplex₂.totalAux.d₂_eq 📋 Mathlib.Algebra.Homology.TotalComplex
{C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h') - HomologicalComplex₂.d₁_eq 📋 Mathlib.Algebra.Homology.TotalComplex
{C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotal c₁₂ i₁' i₂ i₁₂ h') - HomologicalComplex₂.totalAux.d₁_eq' 📋 Mathlib.Algebra.Homology.TotalComplex
{C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂) - HomologicalComplex₂.totalAux.d₁_eq 📋 Mathlib.Algebra.Homology.TotalComplex
{C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h') - HomologicalComplex.mapBifunctor.d₂_eq' 📋 Mathlib.Algebra.Homology.Bifunctor
{C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (j : J) : HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j = c₁.ε₂ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) (K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂' j) - HomologicalComplex.mapBifunctor.d₂_eq 📋 Mathlib.Algebra.Homology.Bifunctor
{C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (j : J) (h' : c₁.π c₂ c (i₁, i₂') = j) : HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j = c₁.ε₂ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h') - HomologicalComplex.mapBifunctor.d₁_eq' 📋 Mathlib.Algebra.Homology.Bifunctor
{C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) : HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) (K₁.ιMapBifunctorOrZero K₂ F c i₁' i₂ j) - HomologicalComplex.mapBifunctor.d₁_eq 📋 Mathlib.Algebra.Homology.Bifunctor
{C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) (h' : c₁.π c₂ c (i₁', i₂) = j) : HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h') - HomologicalComplex.mapBifunctor₁₂.d₃_eq 📋 Mathlib.Algebra.Homology.BifunctorAssociator
{C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) {i₃ i₃' : ι₃} (h₃ : c₃.Rel i₃ i₃') (j : ι₄) : HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = c₁₂.ε₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) • CategoryTheory.CategoryStruct.comp ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ i₃')) (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃' j) - HomologicalComplex.mapBifunctor₁₂.d₂_eq 📋 Mathlib.Algebra.Homology.BifunctorAssociator
{C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) {i₂ i₂' : ι₂} (h₂ : c₂.Rel i₂ i₂') (i₃ : ι₃) (j : ι₄) : HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) • CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.obj (K₁.X i₁)).map (K₂.d i₂ i₂'))).app (K₃.X i₃)) (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂' i₃ j) - HomologicalComplex.mapBifunctor₂₃.d₁_eq 📋 Mathlib.Algebra.Homology.BifunctorAssociator
{C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] {i₁ i₁' : ι₁} (h₁ : c₁.Rel i₁ i₁') (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) : HomologicalComplex.mapBifunctor₂₃.d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = c₁.ε₁ c₂₃ c₄ (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) • CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃))) (HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁' i₂ i₃ j) - HomologicalComplex.mapBifunctor₁₂.d₁_eq 📋 Mathlib.Algebra.Homology.BifunctorAssociator
{C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] {i₁ i₁' : ι₁} (h₁ : c₁.Rel i₁ i₁') (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) : HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) • CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.map (K₁.d i₁ i₁')).app (K₂.X i₂))).app (K₃.X i₃)) (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁' i₂ i₃ j) - HomologicalComplex.mapBifunctor₂₃.d₃_eq 📋 Mathlib.Algebra.Homology.BifunctorAssociator
{C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) {i₃ i₃' : ι₃} (h₃ : c₃.Rel i₃ i₃') (j : ι₄) : HomologicalComplex.mapBifunctor₂₃.d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = (c₁.ε₂ c₂₃ c₄ (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)) • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map ((G₂₃.obj (K₂.X i₂)).map (K₃.d i₃ i₃'))) (HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃' j) - HomologicalComplex.mapBifunctor₂₃.d₂_eq 📋 Mathlib.Algebra.Homology.BifunctorAssociator
{C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) {i₂ i₂' : ι₂} (h₂ : c₂.Rel i₂ i₂') (i₃ : ι₃) (j : ι₄) : HomologicalComplex.mapBifunctor₂₃.d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = (c₁.ε₂ c₂₃ c₄ (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃)) • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map ((G₂₃.map (K₂.d i₂ i₂')).app (K₃.X i₃))) (HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂' i₃ j) - HomologicalComplex₂.ιTotal_totalFlipIso_f_hom 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
{C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₂.π c₁ c (i₂, i₁) = j) : CategoryTheory.CategoryStruct.comp (K.flip.ιTotal c i₂ i₁ j h) ((K.totalFlipIso c).hom.f j) = c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯ - HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
{C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₂.π c₁ c (i₂, i₁) = j) {Z : C} (h✝ : (K.total c).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.flip.ιTotal c i₂ i₁ j h) (CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) h✝) = CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) h✝ - HomologicalComplex₂.ιTotal_totalFlipIso_f_inv 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
{C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j) : CategoryTheory.CategoryStruct.comp (K.ιTotal c i₁ i₂ j h) ((K.totalFlipIso c).inv.f j) = c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯ - HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
{C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j) {Z : C} (h✝ : (K.flip.total c).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal c i₁ i₂ j h) (CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).inv.f j) h✝) = CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) h✝ - HomologicalComplex₂.totalFlipIsoX.eq_1 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
{C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c] [DecidableEq J] (j : J) : K.totalFlipIsoX c j = { hom := K.flip.totalDesc fun i₂ i₁ h => c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯, inv := K.totalDesc fun i₁ i₂ h => c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ } - HomologicalComplex.mapBifunctorMapHomotopy.hom₁.eq_1 📋 Mathlib.Algebra.Homology.BifunctorHomotopy
{C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [DecidableEq J] [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (j j' : J) : HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j' = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).totalDesc fun i₁ i₂ x => c₁.ε₁ c₂ c (c₁.prev i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂)) (L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j')) - HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁ 📋 Mathlib.Algebra.Homology.BifunctorHomotopy
{C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [DecidableEq J] [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J) (h : c₁.π c₂ c (i₁', i₂) = j) (h' : c₁.prev i₁' = i₁) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h) (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j') = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j')) - HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc 📋 Mathlib.Algebra.Homology.BifunctorHomotopy
{C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [DecidableEq J] [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J) (h : c₁.π c₂ c (i₁', i₂) = j) (h' : c₁.prev i₁' = i₁) {Z : D} (h✝ : (L₁.mapBifunctor L₂ F c).X j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j') h✝) = CategoryTheory.CategoryStruct.comp (c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'))) h✝ - HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux 📋 Mathlib.Algebra.Homology.BifunctorHomotopy
{C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [DecidableEq J] [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] {i₁ i₁' : I₁} (hi₁ : c₁.Rel i₁ i₁') {i₂ i₂' : I₂} (hi₂ : c₂.Rel i₂ i₂') (j : J) (hj : c₁.π c₂ c (i₁', i₂) = j) : c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j)) = -CategoryTheory.CategoryStruct.comp ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j)) (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c (c.next j) j) - CochainComplex.shiftFunctor_obj_d 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) (K : CochainComplex C ℤ) (x✝ x✝¹ : ℤ) : ((CochainComplex.shiftFunctor C n).obj K).d x✝ x✝¹ = n.negOnePow • K.d (x✝ + n) (x✝¹ + n) - CochainComplex.shiftFunctor_obj_d' 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n i j : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = n.negOnePow • K.d (i + { as := n }.as) (j + { as := n }.as) - CochainComplex.shiftFunctor_map_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) {X✝ Y✝ : CochainComplex C ℤ} (φ : X✝ ⟶ Y✝) (x✝ : ℤ) : ((CochainComplex.shiftFunctor C n).map φ).f x✝ = φ.f (x✝ + n) - HomologicalComplex₂.D₁_totalShift₁XIso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁') - HomologicalComplex₂.D₁_totalShift₂XIso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁') - HomologicalComplex₂.D₂_totalShift₁XIso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁') - HomologicalComplex₂.D₂_totalShift₂XIso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁') - HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')) h - HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')) h - HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')) h - HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')) h - HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) x).mapIso (K.totalShift₂Iso y) = (x * y).negOnePow • HomologicalComplex₂.total.mapIso ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).app K) (ComplexShape.up ℤ) ≪≫ ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y ≪≫ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).mapIso (K.totalShift₁Iso x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).app (K.total (ComplexShape.up ℤ)) - HomologicalComplex₂.ι_totalShift₂Iso_inv_f 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (b' n' : ℤ) (hb' : a + b' = n') (hn' : n' = n + y) : CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' hb') (CategoryTheory.CategoryStruct.comp (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv ((K.totalShift₂Iso y).inv.f n)) = (a * y).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' ⋯).inv (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h) - HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (b' n' : ℤ) (hb' : a + b' = n') (hn' : n' = n + y) {Z : C} (h✝ : (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).total (ComplexShape.up ℤ)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' hb') (CategoryTheory.CategoryStruct.comp (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv (CategoryTheory.CategoryStruct.comp ((K.totalShift₂Iso y).inv.f n) h✝)) = CategoryTheory.CategoryStruct.comp ((a * y).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' ⋯).inv (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h)) h✝ - HomologicalComplex₂.ι_totalShift₂Iso_hom_f 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (b' : ℤ) (hb' : b' = b + y) (n' : ℤ) (hn' : n' = n + y) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h) ((K.totalShift₂Iso y).hom.f n) = (a * y).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' hb').hom (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' ⋯) (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv) - HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (b' : ℤ) (hb' : b' = b + y) (n' : ℤ) (hn' : n' = n + y) {Z : C} (h✝ : ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (K.total (ComplexShape.up ℤ))).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h) (CategoryTheory.CategoryStruct.comp ((K.totalShift₂Iso y).hom.f n) h✝) = CategoryTheory.CategoryStruct.comp ((a * y).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' hb').hom (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' ⋯) (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv)) h✝ - HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (K.totalShift₂Iso y).hom) = (x * y).negOnePow • CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).hom.app K) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (K.totalShift₁Iso x).hom) ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (ComplexShape.up ℤ))))) - HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (K.total (ComplexShape.up ℤ))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (K.totalShift₂Iso y).hom) h) = CategoryTheory.CategoryStruct.comp ((x * y).negOnePow • CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).hom.app K) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (K.totalShift₁Iso x).hom) ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (ComplexShape.up ℤ)))))) h - CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso 📋 Mathlib.Algebra.Homology.BifunctorShift
{C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_4, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (x y : ℤ) [K₁.HasMapBifunctor K₂ F] : K₁.mapBifunctorShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).mapIso (K₁.mapBifunctorShift₂Iso K₂ F y) = (x * y).negOnePow • ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorShift₂Iso K₂ F y ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).mapIso (K₁.mapBifunctorShift₁Iso K₂ F x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex D ℤ) x y).app (K₁.mapBifunctor K₂ F) - CochainComplex.HomComplex.δ_zero_cochain_comp 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (m₂ : ℤ) (h₂ : n₂ + 1 = m₂) : CochainComplex.HomComplex.δ n₂ m₂ (z₁.comp z₂ ⋯) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ 0 1 z₁).comp z₂ ⋯ - CochainComplex.HomComplex.δ_comp 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (m₁ m₂ m₁₂ : ℤ) (h₁₂ : n₁₂ + 1 = m₁₂) (h₁ : n₁ + 1 = m₁) (h₂ : n₂ + 1 = m₂) : CochainComplex.HomComplex.δ n₁₂ m₁₂ (z₁.comp z₂ h) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ ⋯ - CochainComplex.HomComplex.δ_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + m = q) (q₁ q₂ : ℤ) (hq₁ : q₁ = q - 1) (hq₂ : p + 1 = q₂) : (CochainComplex.HomComplex.δ n m z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p q₁ ⋯) (G.d q₁ q) + m.negOnePow • CategoryTheory.CategoryStruct.comp (F.d p q₂) (z.v q₂ q ⋯) - CochainComplex.mappingCone.descCocycle 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cocycle G K n) (h : m + 1 = n) (eq : CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯) : CochainComplex.HomComplex.Cocycle (CochainComplex.mappingCone φ) K n - CochainComplex.mappingCone.descCocycle_coe 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cocycle G K n) (h : m + 1 = n) (eq : CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯) : ↑(CochainComplex.mappingCone.descCocycle φ α β h eq) = CochainComplex.mappingCone.descCochain φ α (↑β) h - CochainComplex.mappingCone.δ_descCochain 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n) (n' : ℤ) (hn' : n + 1 = n') : CochainComplex.HomComplex.δ n n' (CochainComplex.mappingCone.descCochain φ α β h) = (↑(CochainComplex.mappingCone.fst φ)).comp (CochainComplex.HomComplex.δ m n α + n'.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp β ⋯) ⋯ + (CochainComplex.mappingCone.snd φ).comp (CochainComplex.HomComplex.δ n n' β) ⋯ - CochainComplex.HomComplex.Cochain.δ_leftUnshift 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {a n' : ℤ} (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (m m' : ℤ) (hm' : m + a = m') : CochainComplex.HomComplex.δ n m (γ.leftUnshift n hn) = a.negOnePow • (CochainComplex.HomComplex.δ n' m' γ).leftUnshift m hm' - CochainComplex.HomComplex.Cochain.δ_rightUnshift 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {a n' : ℤ} (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) (m m' : ℤ) (hm' : m' + a = m) : CochainComplex.HomComplex.δ n m (γ.rightUnshift n hn) = a.negOnePow • (CochainComplex.HomComplex.δ n' m' γ).rightUnshift m hm' - CochainComplex.HomComplex.Cochain.δ_leftShift 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' m' : ℤ) (hn' : n + a = n') (m : ℤ) (hm' : m + a = m') : CochainComplex.HomComplex.δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).leftShift a m' hm' - CochainComplex.HomComplex.Cochain.δ_rightShift 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a = m) : CochainComplex.HomComplex.δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).rightShift a m' hm' - CochainComplex.HomComplex.Cochain.leftShift_comp 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L M : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n') {m t t' : ℤ} (γ' : CochainComplex.HomComplex.Cochain L M m) (h : n + m = t) (ht' : t + a = t') : (γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯ - CochainComplex.HomComplex.Cochain.leftShift_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n') (p q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p' + n = q) : (γ.leftShift a n' hn').v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p p' ⋯).hom (γ.v p' q hp') - CochainComplex.HomComplex.Cochain.leftShift_rightShift 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) : (γ.rightShift a n' hn').leftShift a n hn' = (a * n + a * (a - 1) / 2).negOnePow • γ.shift a - CochainComplex.HomComplex.Cochain.rightShift_leftShift 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n') : (γ.leftShift a n' hn').rightShift a n hn' = (a * n' + a * (a - 1) / 2).negOnePow • γ.shift a - CochainComplex.HomComplex.Cochain.δ_shift 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a m : ℤ) : CochainComplex.HomComplex.δ n m (γ.shift a) = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).shift a - CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' n'' : ℤ) (hn' : n' + a = n) (hn'' : n + a = n'') : (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn'' - CochainComplex.HomComplex.Cochain.leftUnshift_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p' + n' = q) : (γ.leftUnshift n hn).v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p' p ⋯).inv (γ.v p' q ⋯) - CategoryTheory.Pretriangulated.Triangle.shiftFunctor_obj 📋 Mathlib.CategoryTheory.Triangulated.TriangleShift
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (n : ℤ) (T : CategoryTheory.Pretriangulated.Triangle C) : (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).obj T = CategoryTheory.Pretriangulated.Triangle.mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₁) (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₂) (n.negOnePow • CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map T.mor₃) ((CategoryTheory.shiftFunctorComm C 1 n).hom.app T.obj₁)) - CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.TriangleShift
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X✝ Y✝ : CategoryTheory.Pretriangulated.Triangle C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₁ = (CategoryTheory.shiftFunctor C n).map f.hom₁ - CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.TriangleShift
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X✝ Y✝ : CategoryTheory.Pretriangulated.Triangle C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₂ = (CategoryTheory.shiftFunctor C n).map f.hom₂ - CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.TriangleShift
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X✝ Y✝ : CategoryTheory.Pretriangulated.Triangle C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₃ = (CategoryTheory.shiftFunctor C n).map f.hom₃ - CochainComplex.mappingCone.shiftIso.eq_1 📋 Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
{C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) : CochainComplex.mappingCone.shiftIso φ n = { hom := CochainComplex.mappingCone.lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (CochainComplex.mappingCone.fst φ).shift n) ((CochainComplex.mappingCone.snd φ).shift n) ⋯, inv := CochainComplex.mappingCone.desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (CochainComplex.mappingCone.inl φ).shift n) ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (CochainComplex.mappingCone.inr φ)) ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ } - CategoryTheory.Triangulated.Subcategory.smul_mem_W_iff 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (S : CategoryTheory.Triangulated.Subcategory C) {X Y : C} (f : X ⟶ Y) (n : ℤˣ) : S.W (n • f) ↔ S.W f - CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁ 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
(C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃ 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
(C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁ 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
(C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv - CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃ 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
(C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv - CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁ 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
(C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃ 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
(C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁ 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
(C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv - CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃ 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
(C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv - CochainComplex.liftCycles_shift_homologyπ 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i) (j : ℤ) (hj : (ComplexShape.up ℤ).next i = j) (hf : CategoryTheory.CategoryStruct.comp f (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j) = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ) (hj' : (ComplexShape.up ℤ).next i' = j') : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) f j hj hf) (HomologicalComplex.homologyπ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K (CategoryTheory.CategoryStruct.comp f (K.shiftFunctorObjXIso n i i' ⋯).hom) j' hj' ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i') (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i i' hi').inv.app K)) - CochainComplex.liftCycles_shift_homologyπ_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i) (j : ℤ) (hj : (ComplexShape.up ℤ).next i = j) (hf : CategoryTheory.CategoryStruct.comp f (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j) = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ) (hj' : (ComplexShape.up ℤ).next i' = j') {Z : C} (h : HomologicalComplex.homology ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) f j hj hf) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K (CategoryTheory.CategoryStruct.comp f (K.shiftFunctorObjXIso n i i' ⋯).hom) j' hj' ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i') (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i i' hi').inv.app K) h)) - AbsoluteValue.map_units_int_smul 📋 Mathlib.Data.Int.AbsoluteValue
{R : Type u_1} {S : Type u_2} [Ring R] [LinearOrderedCommRing S] (abv : AbsoluteValue R S) (x : ℤˣ) (y : R) : abv (x • y) = abv y - HNNExtension.NormalWord.group_smul_toList 📋 Mathlib.GroupTheory.HNNExtension
{G : Type u_1} [Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (w : HNNExtension.NormalWord d) : (g • w).toList = w.toList - HNNExtension.NormalWord.t_smul_eq_unitsSMul 📋 Mathlib.GroupTheory.HNNExtension
{G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (w : HNNExtension.NormalWord d) : HNNExtension.t • w = HNNExtension.NormalWord.unitsSMul φ 1 w - HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul 📋 Mathlib.GroupTheory.HNNExtension
{G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ℤˣ) (w : HNNExtension.NormalWord d) : HNNExtension.t ^ ↑u • w = HNNExtension.NormalWord.unitsSMul φ u w - HNNExtension.NormalWord.smul_cons 📋 Mathlib.GroupTheory.HNNExtension
{G : Type u_1} [Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g₁ g₂ : G) (u : ℤˣ) (w : HNNExtension.NormalWord d) (h1 : w.head ∈ d.set u) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') : g₁ • HNNExtension.NormalWord.cons g₂ u w h1 h2 = HNNExtension.NormalWord.cons (g₁ * g₂) u w h1 h2 - HNNExtension.NormalWord.unitsSMul.eq_1 📋 Mathlib.GroupTheory.HNNExtension
{G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ℤˣ) (w : HNNExtension.NormalWord d) : HNNExtension.NormalWord.unitsSMul φ u w = if h : HNNExtension.NormalWord.Cancels u w then HNNExtension.NormalWord.unitsSMulWithCancel φ u w h else let g' := HNNExtension.NormalWord.unitsSMulGroup φ d u w.head; HNNExtension.NormalWord.cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯ - HNNExtension.NormalWord.unitsSMul_one_group_smul 📋 Mathlib.GroupTheory.HNNExtension
{G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (g : ↥A) (w : HNNExtension.NormalWord d) : HNNExtension.NormalWord.unitsSMul φ 1 (↑g • w) = ↑(φ g) • HNNExtension.NormalWord.unitsSMul φ 1 w - HNNExtension.NormalWord.unitsSMulWithCancel.eq_1 📋 Mathlib.GroupTheory.HNNExtension
{G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ℤˣ) (w : HNNExtension.NormalWord d) : HNNExtension.NormalWord.unitsSMulWithCancel φ u w = HNNExtension.NormalWord.consRecOn (motive := fun x => HNNExtension.NormalWord.Cancels u x → HNNExtension.NormalWord d) w (id fun g a => w) fun g x w x_1 x_2 x_3 can => ↑((HNNExtension.toSubgroupEquiv φ u) ⟨g, ⋯⟩) • w - AlternatingMap.domCoprod.summand_mk'' 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
{ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm (ιa ⊕ ιb)) : AlternatingMap.domCoprod.summand a b (Quotient.mk'' σ) = Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b) - AlternatingMap.domCoprod.summand.eq_1 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
{ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm.ModSumCongr ιa ιb) : AlternatingMap.domCoprod.summand a b σ = Quotient.liftOn' σ (fun σ => Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) ⋯ - MultilinearMap.domCoprod_alternization_coe 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
{ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : MultilinearMap R' (fun x => Mᵢ) N₁) (b : MultilinearMap R' (fun x => Mᵢ) N₂) : (↑(MultilinearMap.alternatization a)).domCoprod ↑(MultilinearMap.alternatization b) = ∑ σa : Equiv.Perm ιa, ∑ σb : Equiv.Perm ιb, Equiv.Perm.sign σa • Equiv.Perm.sign σb • (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.domDomCongr σb b) - TensorProduct.gradedComm_of_tmul_of 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
(R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (i j : ι) (a : 𝒜 i) (b : ℬ j) : (TensorProduct.gradedComm R 𝒜 ℬ) ((DirectSum.lof R ι 𝒜 i) a ⊗ₜ[R] (DirectSum.lof R ι ℬ j) b) = (-1) ^ (j * i) • (DirectSum.lof R ι ℬ j) b ⊗ₜ[R] (DirectSum.lof R ι 𝒜 i) a - TensorProduct.gradedCommAux_lof_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
(R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (i j : ι) (a : 𝒜 i) (b : ℬ j) : (TensorProduct.gradedCommAux R 𝒜 ℬ) ((DirectSum.lof R (ι × ι) (fun i => TensorProduct R (𝒜 i.1) (ℬ i.2)) (i, j)) (a ⊗ₜ[R] b)) = (-1) ^ (j * i) • (DirectSum.lof R (ι × ι) (fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) (j, i)) (b ⊗ₜ[R] a) - TensorProduct.gradedCommAux.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
(R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : TensorProduct.gradedCommAux R 𝒜 ℬ = DirectSum.toModule R (ι × ι) (DirectSum (ι × ι) fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) fun i => let_fun o := DirectSum.lof R (ι × ι) (fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) i.swap; let_fun s := (-1) ^ (i.1 * i.2); (s • o) ∘ₗ ↑(TensorProduct.comm R (𝒜 i.1) (ℬ i.2)) - TensorProduct.algebraMap_gradedMul 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
{R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (r : R) (x : TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i)) : ((TensorProduct.gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) x = r • x - TensorProduct.gradedMul_algebraMap 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
{R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (x : TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i)) (r : R) : ((TensorProduct.gradedMul R 𝒜 ℬ) x) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • x - TensorProduct.tmul_of_gradedMul_of_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
(R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (j₁ i₂ : ι) (a₁ : DirectSum ι fun i => 𝒜 i) (b₁ : ℬ j₁) (a₂ : 𝒜 i₂) (b₂ : DirectSum ι fun i => ℬ i) : ((TensorProduct.gradedMul R 𝒜 ℬ) (a₁ ⊗ₜ[R] (DirectSum.lof R ι ℬ j₁) b₁)) ((DirectSum.lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) = (-1) ^ (j₁ * i₂) • (a₁ * (DirectSum.lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((DirectSum.lof R ι ℬ j₁) b₁ * b₂) - GradedTensorProduct.lift 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
{R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {C : Type u_5} [Ring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)) : GradedTensorProduct R 𝒜 ℬ →ₐ[R] C - GradedTensorProduct.tmul_coe_mul_coe_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
{R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {j₁ i₂ : ι} (a₁ : A) (b₁ : ↥(ℬ j₁)) (a₂ : ↥(𝒜 i₂)) (b₂ : B) : a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (-1) ^ (j₁ * i₂) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂) - GradedTensorProduct.liftEquiv 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
{R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {C : Type u_5} [Ring C] [Algebra R C] : { fg // ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) } ≃ (GradedTensorProduct R 𝒜 ℬ →ₐ[R] C) - GradedTensorProduct.lift_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
{R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {C : Type u_5} [Ring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)) (a : A) (b : B) : (GradedTensorProduct.lift 𝒜 ℬ f g h_anti_commutes) (a ᵍ⊗ₜ[R] b) = f a * g b - GradedTensorProduct.comm_coe_tmul_coe 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
{R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {i j : ι} (a : ↥(𝒜 i)) (b : ↥(ℬ j)) : (GradedTensorProduct.comm 𝒜 ℬ) (↑a ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • ↑b ᵍ⊗ₜ[R] ↑a - CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd 📋 Mathlib.LinearAlgebra.CliffordAlgebra.Prod
{R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁ →qᵢ Qₙ) (f₂ : Q₂ →qᵢ Qₙ) (hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)) (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₁ i₂ : ZMod 2} (hm₁ : m₁ ∈ CliffordAlgebra.evenOdd Q₁ i₁) (hm₂ : m₂ ∈ CliffordAlgebra.evenOdd Q₂ i₂) : (CliffordAlgebra.map f₁) m₁ * (CliffordAlgebra.map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((CliffordAlgebra.map f₂) m₂ * (CliffordAlgebra.map f₁) m₁) - Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det' 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Misc
{R : Type u_1} [CommRing R] {n : ℕ} (M : Matrix (Fin n) (Fin (n + 1)) R) (hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0) (j₁ j₂ : Fin (n + 1)) : (M.submatrix id j₁.succAbove).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det - Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Misc
{R : Type u_1} [CommRing R] {n : ℕ} (M : Matrix (Fin (n + 1)) (Fin n) R) (hv : ∑ j : Fin (n + 1), M j = 0) (j₁ j₂ : Fin (n + 1)) : (M.submatrix j₁.succAbove id).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix j₂.succAbove id).det - ContinuousMultilinearMap.alternatization_apply_apply 📋 Mathlib.Topology.Algebra.Module.Alternating.Basic
{R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun x => M) N) (v : ι → M) : (ContinuousMultilinearMap.alternatization f) v = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • f (v ∘ ⇑σ) - ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap 📋 Mathlib.Topology.Algebra.Module.Alternating.Basic
{R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun x => M) N) : (ContinuousMultilinearMap.alternatization f).toContinuousMultilinearMap = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • ContinuousMultilinearMap.domDomCongr σ f - ContinuousMultilinearMap.alternatization.eq_1 📋 Mathlib.Topology.Algebra.Module.Alternating.Basic
{R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] : ContinuousMultilinearMap.alternatization = { toFun := fun f => { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • ContinuousMultilinearMap.domDomCongr σ f, map_eq_zero_of_eq' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
woould find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision 4e1aab0 serving mathlib revision 83ce5b0