tensorUnitIso — Mathlib

Lean4
/-- As a graded object, the single complex `(single C c 0).obj (𝟙_ C)` identifies
to the unit `(GradedObject.single₀ I).obj (𝟙_ C)` of the tensor product of graded objects. -/
noncomputable def tensorUnitIso : (GradedObject.single₀ I).obj (𝟙_ C) ≅ (tensorUnit C c).X :=
  GradedObject.isoMk _ _
    (fun i ↦
      if hi : i = 0 then
        (GradedObject.singleObjApplyIsoOfEq (0 : I) (𝟙_ C) i hi).trans (singleObjXIsoOfEq c 0 (𝟙_ C) i hi).symm
      else
        { hom := 0
          inv := 0
          hom_inv_id := (GradedObject.isInitialSingleObjApply 0 (𝟙_ C) i hi).hom_ext _ _
          inv_hom_id := (isZero_single_obj_X c 0 (𝟙_ C) i hi).eq_of_src _ _ })
Похожие утверждения