Loogle!

Result

Found 13 declarations mentioning CochainComplex.mappingCone.map.

• CochainComplex.mappingCone.triangleMap_hom₃ 📋 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₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁) (φ₂ : K₂ ⟶ L₂) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂) (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂) : (CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₃ = CochainComplex.mappingCone.map φ₁ φ₂ a b comm
• CochainComplex.mappingCone.map 📋 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₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁) (φ₂ : K₂ ⟶ L₂) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂) (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂) : CochainComplex.mappingCone φ₁ ⟶ CochainComplex.mappingCone φ₂
• CochainComplex.mappingCone.map.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₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁) (φ₂ : K₂ ⟶ L₂) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂) (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂) : CochainComplex.mappingCone.map φ₁ φ₂ a b comm = CochainComplex.mappingCone.desc φ₁ ((CochainComplex.HomComplex.Cochain.ofHom a).comp (CochainComplex.mappingCone.inl φ₂) CochainComplex.mappingCone.homotopyToZeroOfId._proof_7) (CategoryTheory.CategoryStruct.comp b (CochainComplex.mappingCone.inr φ₂)) ⋯
• CochainComplex.mappingCone.map_eq_mapOfHomotopy 📋 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₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁) (φ₂ : K₂ ⟶ L₂) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂) (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂) : CochainComplex.mappingCone.map φ₁ φ₂ a b comm = CochainComplex.mappingCone.mapOfHomotopy (Homotopy.ofEq comm)
• CochainComplex.mappingCone.map_id 📋 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) : CochainComplex.mappingCone.map φ φ (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id L) ⋯ = CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone φ)
• CochainComplex.mappingCone.map_comp 📋 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₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁) (φ₂ : K₂ ⟶ L₂) (φ₃ : K₃ ⟶ L₃) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂) (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂) (a' : K₂ ⟶ K₃) (b' : L₂ ⟶ L₃) (comm' : CategoryTheory.CategoryStruct.comp φ₂ b' = CategoryTheory.CategoryStruct.comp a' φ₃) : CochainComplex.mappingCone.map φ₁ φ₃ (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b') ⋯ = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₂ a b comm) (CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm')
• CochainComplex.mappingCone.map_comp_assoc 📋 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₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁) (φ₂ : K₂ ⟶ L₂) (φ₃ : K₃ ⟶ L₃) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂) (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂) (a' : K₂ ⟶ K₃) (b' : L₂ ⟶ L₃) (comm' : CategoryTheory.CategoryStruct.comp φ₂ b' = CategoryTheory.CategoryStruct.comp a' φ₃) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : CochainComplex.mappingCone φ₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₃ (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b') ⋯) h = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₂ a b comm) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm') h)
• CochainComplex.mappingConeCompTriangle_mor₁ 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : (CochainComplex.mappingConeCompTriangle f g).mor₁ = CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁) g ⋯
• CochainComplex.mappingConeCompTriangle_mor₂ 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : (CochainComplex.mappingConeCompTriangle f g).mor₂ = CochainComplex.mappingCone.map (CategoryTheory.CategoryStruct.comp f g) g f (CategoryTheory.CategoryStruct.id X₃) ⋯
• CochainComplex.mappingConeCompTriangle_mor₃_naturality 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Y₁ Y₂ Y₃ : CochainComplex C ℤ} (f' : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map g g' (φ.app 1) (φ.app 2) ⋯) (CochainComplex.mappingConeCompTriangle f' g').mor₃ = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₃ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.map f f' (φ.app 0) (φ.app 1) ⋯))
• CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Y₁ Y₂ Y₃ : CochainComplex C ℤ} (f' : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingConeCompTriangle f' g').obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map g g' (φ.app 1) (φ.app 2) ⋯) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f' g').mor₃ h) = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₃ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.map f f' (φ.app 0) (φ.app 1) ⋯)) h)
• CochainComplex.mappingConeCompHomotopyEquiv_comm₁ 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁) g ⋯)) (CochainComplex.mappingConeCompHomotopyEquiv f g).inv = (CochainComplex.mappingConeCompTriangle f g).mor₂
• CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Z : CochainComplex C ℤ} (h : CochainComplex.mappingCone g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁) g ⋯)) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).inv h) = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₂ h

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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 ?a

   If 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 ?b

4. By 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 find tsum_lt_tsum even though the hypothesis f i < g i is 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, _ * _, _ ^ _, |- _ < _ → _
would 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 19971e9 serving mathlib revision bce1d65