Z — Mathlib · SciLib

Lean4
/-- Auxiliary definition for `FunctorialFactorizationData.functorCategory`. -/
@[simps]
def Z : Arrow (J ⥤ C) ⥤ J ⥤ C
    where
  obj
    f :=
    { obj := fun j => (data.factorizationData (f.hom.app j)).Z
      map := fun φ =>
        data.mapZ
          { left := f.left.map φ
            right := f.right.map φ }
      map_id := fun j => by
        dsimp
        rw [← data.mapZ_id (f.hom.app j)]
        congr <;> simp
      map_comp := fun _ _ => by
        dsimp
        rw [← data.mapZ_comp]
        congr <;> simp }
  map
    τ :=
    { app := fun j =>
        data.mapZ
          { left := τ.left.app j
            right := τ.right.app j
            w := congr_app τ.w j }
      naturality := fun _ _ α => by
        dsimp
        rw [← data.mapZ_comp, ← data.mapZ_comp]
        congr 1
        ext <;> simp }
  map_id
    f := by
    ext j
    dsimp
    rw [← data.mapZ_id]
    congr 1
  map_comp f
    g := by
    ext j
    dsimp
    rw [← data.mapZ_comp]
    congr 1
Похожие утверждения