map — Mathlib

Lean4
/-- The CoGrothendieck construction is functorial: a strong natural transformation `α : F ⟶ G`
induces a functor `CoGrothendieck.map : ∫ᶜ F ⥤ ∫ᶜ G`. -/
@[simps!]
def map (α : F ⟶ G) : ∫ᶜ F ⥤ ∫ᶜ G
    where
  obj
    a :=
    { base := a.base
      fiber := (α.app ⟨op a.base⟩).obj a.fiber }
  map {a b}
    f :=
    { base := f.1
      fiber := (α.app ⟨op a.base⟩).map f.2 ≫ (α.naturality f.1.op.toLoc).hom.app b.fiber }
  map_id
    a := by
    ext1
    · dsimp
    · simp [StrongTrans.naturality_id_hom_app, ← Functor.map_comp_assoc]
  map_comp {a b c} f
    g := by
    ext
    · dsimp
    · dsimp
      simp only [StrongTrans.naturality_comp_hom_app, map_comp, assoc, comp_id]
      slice_lhs 2 4 => simp only [← Functor.map_comp, Iso.inv_hom_id_app, Cat.comp_obj, comp_id]
      simp [← Functor.comp_map]
Похожие утверждения