Γ₀_obj_termwise_mapMono_comp_PInfty

English

For a simplicial object X in a preadditive category, the termwise mapMono at level Δ to Δ' respects the PInfty filtration; i.e., the map on the summand indexed by Δ is equal to the composition of PInfty.f and X.map i.op with the appropriate γ-structure.

Русский

Для симплициального объекта X в преддобавительной категории отображение на суммантy по уровню Δ к Δ' сохраняет филтрацию PInfty; т.е. отображение на суммонду, индексируемую по Δ, равняется композиции PInfty.f и X.map i.op с соответствующей структурой γ.

LaTeX

$$$Γ_0.Obj.Termwise.mapMono (AlternatingFaceMapComplex.obj X) i \;\;≃\; PInfty.f Δ.len \;\circ X.map i.op$$$

Lean4

@[reassoc]
theorem Γ₀_obj_termwise_mapMono_comp_PInfty (X : SimplicialObject C) {Δ Δ' : SimplexCategory} (i : Δ ⟶ Δ') [Mono i] :
    Γ₀.Obj.Termwise.mapMono (AlternatingFaceMapComplex.obj X) i ≫ PInfty.f Δ.len = PInfty.f Δ'.len ≫ X.map i.op :=
  by
  induction Δ using SimplexCategory.rec with
  | _ n
  induction Δ' using SimplexCategory.rec with
  | _ n'
  dsimp
    -- We start with the case `i` is an identity

  by_cases h : n = n'
  · subst h
    simp only [SimplexCategory.eq_id_of_mono i, Γ₀.Obj.Termwise.mapMono_id, op_id, X.map_id]
    dsimp
    simp only [id_comp, comp_id]
  by_cases hi : Isδ₀ i
  · have h' : n' = n + 1 := hi.left
    subst h'
    simp only [Γ₀.Obj.Termwise.mapMono_δ₀' _ i hi]
    dsimp
    rw [← PInfty.comm _ n, AlternatingFaceMapComplex.obj_d_eq]
    simp only [Preadditive.comp_sum]
    rw [Finset.sum_eq_single (0 : Fin (n + 2))]
    rotate_left
    · intro b _ hb
      rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_zero]
    · simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff]
    · simp only [hi.eq_δ₀, Fin.val_zero, pow_zero, one_zsmul]
      rfl
        -- The case `i ≠ δ 0`

  · rw [Γ₀.Obj.Termwise.mapMono_eq_zero _ i _ hi, zero_comp]
    swap
    · by_contra h'
      exact h (congr_arg SimplexCategory.len h'.symm)
    rw [PInfty_comp_map_mono_eq_zero]
    · exact h
    · assumption

Похожие утверждения