Documentation

Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Iterations of δ 0 and σ 0 #

This file introduces morphisms δ₀Iter i and σ₀Iter i for simplicial objects: they are obtained as the ith iteration of δ 0 or σ 0.

source
def CategoryTheory.SimplicialObject.δ₀Iter {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) {n m : ℕ} (i : ℕ) (hi : n + i = m := by lia) :
X.obj (Opposite.op { len := m }) ⟶ X.obj (Opposite.op { len := n })

If X is a simplicial object and n + i = m, this is the morphism X _⦋m⦌ ⟶ X _⦋n⦌ obtained by iterating i times the face map X.δ 0.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.SimplicialObject.δ₀Iter_zero {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (n : ℕ) :
    X.δ₀Iter 0 ⋯ = CategoryStruct.id (X.obj (Opposite.op { len := n }))
    source
    @[simp]
    theorem CategoryTheory.SimplicialObject.δ₀Iter_one {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (n : ℕ) :
    X.δ₀Iter 1 ⋯ = X.δ 0
    source
    theorem CategoryTheory.SimplicialObject.δ₀Iter_succ {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (h : n + i = m := by lia) :
    X.δ₀Iter (i + 1) ⋯ = CategoryStruct.comp (X.δ 0) (X.δ₀Iter i h)
    source
    theorem CategoryTheory.SimplicialObject.δ₀Iter_succ_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (h : n + i = m := by lia) {Z : C} (h✝ : X.obj (Opposite.op { len := n }) ⟶ Z) :
    CategoryStruct.comp (X.δ₀Iter (i + 1) ⋯) h✝ = CategoryStruct.comp (X.δ 0) (CategoryStruct.comp (X.δ₀Iter i h) h✝)
    source
    theorem CategoryTheory.SimplicialObject.δ₀Iter_succ' {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m := by lia) :
    X.δ₀Iter (i + 1) h = CategoryStruct.comp (X.δ₀Iter i ⋯) (X.δ 0)
    source
    theorem CategoryTheory.SimplicialObject.δ₀Iter_succ'_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m := by lia) {Z : C} (h✝ : X.obj (Opposite.op { len := n }) ⟶ Z) :
    CategoryStruct.comp (X.δ₀Iter (i + 1) h) h✝ = CategoryStruct.comp (X.δ₀Iter i ⋯) (CategoryStruct.comp (X.δ 0) h✝)
    source
    theorem CategoryTheory.SimplicialObject.δ_δ₀Iter {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 2)) (hi : n + i = m := by lia) (hj : ↑j ≤ i := by grind) :
    CategoryStruct.comp (X.δ j) (X.δ₀Iter i hi) = X.δ₀Iter (i + 1) ⋯
    source
    theorem CategoryTheory.SimplicialObject.δ_δ₀Iter_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 2)) (hi : n + i = m := by lia) (hj : ↑j ≤ i := by grind) {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z) :
    CategoryStruct.comp (X.δ j) (CategoryStruct.comp (X.δ₀Iter i hi) h) = CategoryStruct.comp (X.δ₀Iter (i + 1) ⋯) h
    source
    theorem CategoryTheory.SimplicialObject.δ_δ₀Iter' {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m := by lia) (hi'' : ↑i' = ↑i + j := by grind) :
    CategoryStruct.comp (X.δ i') (X.δ₀Iter j ⋯) = CategoryStruct.comp (X.δ₀Iter j ⋯) (X.δ i)
    source
    theorem CategoryTheory.SimplicialObject.δ_δ₀Iter'_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m := by lia) (hi'' : ↑i' = ↑i + j := by grind) {Z : C} (h✝ : X.obj (Opposite.op { len := n }) ⟶ Z) :
    CategoryStruct.comp (X.δ i') (CategoryStruct.comp (X.δ₀Iter j ⋯) h✝) = CategoryStruct.comp (X.δ₀Iter j ⋯) (CategoryStruct.comp (X.δ i) h✝)
    source
    theorem CategoryTheory.SimplicialObject.σ_δ₀Iter {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + (i + 1) = m + 1 := by lia) (hj : ↑j ≤ i := by grind) :
    CategoryStruct.comp (X.σ j) (X.δ₀Iter (i + 1) hi) = X.δ₀Iter i ⋯
    source
    theorem CategoryTheory.SimplicialObject.σ_δ₀Iter_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + (i + 1) = m + 1 := by lia) (hj : ↑j ≤ i := by grind) {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z) :
    CategoryStruct.comp (X.σ j) (CategoryStruct.comp (X.δ₀Iter (i + 1) hi) h) = CategoryStruct.comp (X.δ₀Iter i ⋯) h
    source
    theorem CategoryTheory.SimplicialObject.σ_δ₀Iter' {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m := by lia) (hj' : ↑j = ↑j' + i := by grind) :
    CategoryStruct.comp (X.σ j) (X.δ₀Iter i ⋯) = CategoryStruct.comp (X.δ₀Iter i hi') (X.σ j')
    source
    theorem CategoryTheory.SimplicialObject.σ_δ₀Iter'_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m := by lia) (hj' : ↑j = ↑j' + i := by grind) {Z : C} (h : X.obj (Opposite.op { len := n + 1 }) ⟶ Z) :
    CategoryStruct.comp (X.σ j) (CategoryStruct.comp (X.δ₀Iter i ⋯) h) = CategoryStruct.comp (X.δ₀Iter i hi') (CategoryStruct.comp (X.σ j') h)
    source
    def CategoryTheory.SimplicialObject.σ₀Iter {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) {n m : ℕ} (i : ℕ) (hi : n + i = m := by lia) :
    X.obj (Opposite.op { len := n }) ⟶ X.obj (Opposite.op { len := m })

    If X is a simplicial object and n + i = m, this is the morphism X _⦋n⦌ ⟶ X _⦋m⦌ obtained by iterating i times the degeneracy map X.σ 0.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.SimplicialObject.σ₀Iter_zero {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (n : ℕ) :
      X.σ₀Iter 0 ⋯ = CategoryStruct.id (X.obj (Opposite.op { len := n }))
      source
      @[simp]
      theorem CategoryTheory.SimplicialObject.σ₀Iter_one {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (n : ℕ) :
      X.σ₀Iter 1 ⋯ = X.σ 0
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_succ {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m := by lia) :
      X.σ₀Iter (i + 1) h = CategoryStruct.comp (X.σ 0) (X.σ₀Iter i ⋯)
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_succ_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m := by lia) {Z : C} (h✝ : X.obj (Opposite.op { len := m }) ⟶ Z) :
      CategoryStruct.comp (X.σ₀Iter (i + 1) h) h✝ = CategoryStruct.comp (X.σ 0) (CategoryStruct.comp (X.σ₀Iter i ⋯) h✝)
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_succ' {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (h : n + i = m := by lia) :
      X.σ₀Iter (i + 1) ⋯ = CategoryStruct.comp (X.σ₀Iter i h) (X.σ 0)
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_succ'_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (h : n + i = m := by lia) {Z : C} (h✝ : X.obj (Opposite.op { len := m + 1 }) ⟶ Z) :
      CategoryStruct.comp (X.σ₀Iter (i + 1) ⋯) h✝ = CategoryStruct.comp (X.σ₀Iter i h) (CategoryStruct.comp (X.σ 0) h✝)
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_δ {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (h : m + (j + 1) = n + 1 := by lia) (hi' : ↑i ≤ j + 1 := by grind) :
      CategoryStruct.comp (X.σ₀Iter (j + 1) h) (X.δ i) = X.σ₀Iter j ⋯
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_δ_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (h : m + (j + 1) = n + 1 := by lia) (hi' : ↑i ≤ j + 1 := by grind) {Z : C} (h✝ : X.obj (Opposite.op { len := n }) ⟶ Z) :
      CategoryStruct.comp (X.σ₀Iter (j + 1) h) (CategoryStruct.comp (X.δ i) h✝) = CategoryStruct.comp (X.σ₀Iter j ⋯) h✝
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_δ' {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n := by lia) (hi' : j < ↑i := by grind) (hi'' : ↑i = ↑i' + j := by grind) :
      CategoryStruct.comp (X.σ₀Iter j ⋯) (X.δ i) = CategoryStruct.comp (X.δ i') (X.σ₀Iter j ⋯)
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_δ'_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n := by lia) (hi' : j < ↑i := by grind) (hi'' : ↑i = ↑i' + j := by grind) {Z : C} (h✝ : X.obj (Opposite.op { len := n }) ⟶ Z) :
      CategoryStruct.comp (X.σ₀Iter j ⋯) (CategoryStruct.comp (X.δ i) h✝) = CategoryStruct.comp (X.δ i') (CategoryStruct.comp (X.σ₀Iter j ⋯) h✝)
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_σ {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + i = m := by lia) (hj : ↑j ≤ i := by grind) :
      CategoryStruct.comp (X.σ₀Iter i hi) (X.σ j) = X.σ₀Iter (i + 1) ⋯
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_σ_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : n + i = m := by lia) (hj : ↑j ≤ i := by grind) {Z : C} (h : X.obj (Opposite.op { len := m + 1 }) ⟶ Z) :
      CategoryStruct.comp (X.σ₀Iter i hi) (CategoryStruct.comp (X.σ j) h) = CategoryStruct.comp (X.σ₀Iter (i + 1) ⋯) h
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_σ' {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m := by lia) (hj : ↑j = ↑j' + i := by grind) :
      CategoryStruct.comp (X.σ₀Iter i hi) (X.σ j) = CategoryStruct.comp (X.σ j') (X.σ₀Iter i ⋯)
      source
      theorem CategoryTheory.SimplicialObject.σ₀Iter_σ'_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m := by lia) (hj : ↑j = ↑j' + i := by grind) {Z : C} (h : X.obj (Opposite.op { len := m + 1 }) ⟶ Z) :
      CategoryStruct.comp (X.σ₀Iter i hi) (CategoryStruct.comp (X.σ j) h) = CategoryStruct.comp (X.σ j') (CategoryStruct.comp (X.σ₀Iter i ⋯) h)
      source
      @[simp]
      theorem CategoryTheory.SimplicialObject.σ₀Iter_δ₀Iter {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (hi : n + i = m := by lia) :
      CategoryStruct.comp (X.σ₀Iter i hi) (X.δ₀Iter i hi) = CategoryStruct.id (X.obj (Opposite.op { len := n }))
      source
      @[simp]
      theorem CategoryTheory.SimplicialObject.σ₀Iter_δ₀Iter_assoc {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (hi : n + i = m := by lia) {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z) :
      CategoryStruct.comp (X.σ₀Iter i hi) (CategoryStruct.comp (X.δ₀Iter i hi) h) = h
      source
      instance CategoryTheory.SimplicialObject.instMonoσ₀Iter {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (hi : n + i = m) :
      Mono (X.σ₀Iter i hi)
      source
      instance CategoryTheory.SimplicialObject.instEpiδ₀Iter {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) (i : ℕ) {n m : ℕ} (hi : n + i = m) :
      Epi (X.δ₀Iter i hi)
      source
      @[simp]
      theorem CategoryTheory.SimplicialObject.Augmented.δ₀Iter_hom_app {C : Type u_1} [Category.{v_1, u_1} C] (Y : Augmented C) {n m : ℕ} (i : ℕ) (hi : n + i = m := by lia) :
      CategoryStruct.comp (Y.left.δ₀Iter i hi) (Y.hom.app (Opposite.op { len := n })) = Y.hom.app (Opposite.op { len := m })
      source
      @[simp]
      theorem CategoryTheory.SimplicialObject.Augmented.δ₀Iter_hom_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] (Y : Augmented C) {n m : ℕ} (i : ℕ) (hi : n + i = m := by lia) {Z : C} (h : Y.right ⟶ Z) :
      CategoryStruct.comp (Y.left.δ₀Iter i hi) (CategoryStruct.comp (Y.hom.app (Opposite.op { len := n })) h) = CategoryStruct.comp (Y.hom.app (Opposite.op { len := m })) h
      source
      @[simp]
      theorem CategoryTheory.SimplicialObject.Augmented.σ₀Iter_hom_app {C : Type u_1} [Category.{v_1, u_1} C] (Y : Augmented C) {n m : ℕ} (i : ℕ) (hi : n + i = m := by lia) :
      CategoryStruct.comp (Y.left.σ₀Iter i hi) (Y.hom.app (Opposite.op { len := m })) = Y.hom.app (Opposite.op { len := n })
      source
      @[simp]
      theorem CategoryTheory.SimplicialObject.Augmented.σ₀Iter_hom_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] (Y : Augmented C) {n m : ℕ} (i : ℕ) (hi : n + i = m := by lia) {Z : C} (h : Y.right ⟶ Z) :
      CategoryStruct.comp (Y.left.σ₀Iter i hi) (CategoryStruct.comp (Y.hom.app (Opposite.op { len := m })) h) = CategoryStruct.comp (Y.hom.app (Opposite.op { len := n })) h