Documentation

Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Cochains from or to single complexes #

We introduce constructors Cochain.fromSingleMk and Cocycle.fromSingleMk for cochains and cocycles from a single complex. We also introduce similar definitions for cochains and cocyles to a single complex.

source
noncomputable def CochainComplex.HomComplex.Cochain.fromSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} :
p + n = q → Cochain ((singleFunctor C p).obj X) K n

Constructor for cochains from a single complex.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CochainComplex.HomComplex.Cochain.fromSingleMk_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) (p q n : ℤ) (h : p + n = q) :
    fromSingleMk 0 h = 0
    source
    @[simp]
    theorem CochainComplex.HomComplex.Cochain.fromSingleMk_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
    (fromSingleMk f h).v p q h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).hom f
    source
    theorem CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (p' q' : ℤ) (hpq' : p' + n = q') (hp' : p' ≠ p) :
    (fromSingleMk f h).v p' q' hpq' = 0
    source
    theorem CochainComplex.HomComplex.Cochain.δ_fromSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (n' q' : ℤ) (h' : p + n' = q') :
    δ n n' (fromSingleMk f h) = fromSingleMk (CategoryTheory.CategoryStruct.comp f (K.d q q')) h'
    source
    noncomputable def CochainComplex.HomComplex.Cochain.fromSingleEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q n : ℤ} (h : p + n = q) :
    Cochain ((singleFunctor C p).obj X) K n ≃+ (X ⟶ K.X q)

    Cochains of degree n from (singleFunctor C p).obj X to K identify to X ⟶ K.X q when p + n = q.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CochainComplex.HomComplex.Cochain.fromSingleMk_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
      fromSingleMk (f + g) h = fromSingleMk f h + fromSingleMk g h
      source
      @[simp]
      theorem CochainComplex.HomComplex.Cochain.fromSingleMk_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
      fromSingleMk (f - g) h = fromSingleMk f h - fromSingleMk g h
      source
      @[simp]
      theorem CochainComplex.HomComplex.Cochain.fromSingleMk_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
      fromSingleMk (-f) h = -fromSingleMk f h
      source
      theorem CochainComplex.HomComplex.Cochain.fromSingleMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p n : ℤ} (α : Cochain ((singleFunctor C p).obj X) K n) (q : ℤ) (h : p + n = q) :
      ∃ (f : X ⟶ K.X q), fromSingleMk f h = α
      source
      noncomputable def CochainComplex.HomComplex.Cochain.toSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} :
      p + n = q → Cochain K ((singleFunctor C q).obj X) n

      Constructor for cochains to a single complex.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CochainComplex.HomComplex.Cochain.toSingleMk_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) (p q n : ℤ) (h : p + n = q) :
        toSingleMk 0 h = 0
        source
        @[simp]
        theorem CochainComplex.HomComplex.Cochain.toSingleMk_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) :
        (toSingleMk f h).v p q h = CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv
        source
        theorem CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' q' : ℤ) (hpq' : p' + n = q') (hp' : p' ≠ p) :
        (toSingleMk f h).v p' q' hpq' = 0
        source
        theorem CochainComplex.HomComplex.Cochain.δ_toSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (n' p' : ℤ) (h' : p' + n' = q) :
        δ n n' (toSingleMk f h) = n'.negOnePow • toSingleMk (CategoryTheory.CategoryStruct.comp (K.d p' p) f) h'
        source
        noncomputable def CochainComplex.HomComplex.Cochain.toSingleEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q n : ℤ} (h : p + n = q) :
        Cochain K ((singleFunctor C q).obj X) n ≃+ (K.X p ⟶ X)

        Cochains of degree n from (singleFunctor C q).obj X to K identify to K.X p ⟶ X when p + n = q.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.toSingleMk_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : K.X p ⟶ X) {n : ℤ} (h : p + n = q) :
          toSingleMk (f + g) h = toSingleMk f h + toSingleMk g h
          source
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.toSingleMk_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : K.X p ⟶ X) {n : ℤ} (h : p + n = q) :
          toSingleMk (f - g) h = toSingleMk f h - toSingleMk g h
          source
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.toSingleMk_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) :
          toSingleMk (-f) h = -toSingleMk f h
          source
          theorem CochainComplex.HomComplex.Cochain.toSingleMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {q n : ℤ} (α : Cochain K ((singleFunctor C q).obj X) n) (p : ℤ) (h : p + n = q) :
          ∃ (f : K.X p ⟶ X), toSingleMk f h = α
          source
          noncomputable def CochainComplex.HomComplex.Cocycle.fromSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0) :
          Cocycle ((singleFunctor C p).obj X) K n

          Constructor for cocycles from a single complex.

          Equations
          Instances For
            source
            @[simp]
            theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0) :
            ↑(fromSingleMk f h q' hq' hf) = Cochain.fromSingleMk f h
            source
            theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p n : ℤ} (α : Cocycle ((singleFunctor C p).obj X) K n) (q : ℤ) (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') :
            ∃ (f : X ⟶ K.X q) (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0), fromSingleMk f h q' hq' hf = α
            source
            theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0) (hg : CategoryTheory.CategoryStruct.comp g (K.d q q') = 0) :
            fromSingleMk (f + g) h q' hq' ⋯ = fromSingleMk f h q' hq' hf + fromSingleMk g h q' hq' hg
            source
            theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0) (hg : CategoryTheory.CategoryStruct.comp g (K.d q q') = 0) :
            fromSingleMk (f - g) h q' hq' ⋯ = fromSingleMk f h q' hq' hf - fromSingleMk g h q' hq' hg
            source
            theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0) :
            fromSingleMk (-f) h q' hq' ⋯ = -fromSingleMk f h q' hq' hf
            source
            @[simp]
            theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) {p q n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') :
            fromSingleMk 0 h q' hq' ⋯ = 0
            source
            theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0) (q'' : ℤ) (hq'' : q'' + 1 = q) :
            fromSingleMk f h q' hq' hf ∈ coboundaries ((singleFunctor C p).obj X) K n ↔ ∃ (g : X ⟶ K.X q''), CategoryTheory.CategoryStruct.comp g (K.d q'' q) = f
            source
            noncomputable def CochainComplex.HomComplex.Cocycle.toSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) :
            Cocycle K ((singleFunctor C q).obj X) n

            Constructor for cocycles to a single complex.

            Equations
            Instances For
              source
              @[simp]
              theorem CochainComplex.HomComplex.Cocycle.toSingleMk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) :
              ↑(toSingleMk f h p' hp' hf) = Cochain.toSingleMk f h
              source
              theorem CochainComplex.HomComplex.Cocycle.toSingleMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {q n : ℤ} (α : Cocycle K ((singleFunctor C q).obj X) n) (p : ℤ) (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) :
              ∃ (f : K.X p ⟶ X) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0), toSingleMk f h p' hp' hf = α
              source
              theorem CochainComplex.HomComplex.Cocycle.toSingleMk_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) (hg : CategoryTheory.CategoryStruct.comp (K.d p' p) g = 0) :
              toSingleMk (f + g) h p' hp' ⋯ = toSingleMk f h p' hp' hf + toSingleMk g h p' hp' hg
              source
              theorem CochainComplex.HomComplex.Cocycle.toSingleMk_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) (hg : CategoryTheory.CategoryStruct.comp (K.d p' p) g = 0) :
              toSingleMk (f - g) h p' hp' ⋯ = toSingleMk f h p' hp' hf - toSingleMk g h p' hp' hg
              source
              theorem CochainComplex.HomComplex.Cocycle.toSingleMk_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) :
              toSingleMk (-f) h p' hp' ⋯ = -toSingleMk f h p' hp' hf
              source
              @[simp]
              theorem CochainComplex.HomComplex.Cocycle.toSingleMk_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) {p q n : ℤ} (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) :
              toSingleMk 0 h p' hp' ⋯ = 0
              source
              theorem CochainComplex.HomComplex.Cocycle.toSingleMk_mem_coboundaries_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) (p'' : ℤ) (hp'' : p + 1 = p'') :
              toSingleMk f h p' hp' hf ∈ coboundaries K ((singleFunctor C q).obj X) n ↔ ∃ (g : K.X p'' ⟶ X), CategoryTheory.CategoryStruct.comp (K.d p p'') g = f