additive_of_full_essSurj_comp — Mathlib

English

If F is full and essentially surjective, and G is any functor, then G is additive for the composite F ⋙ G.

Русский

Если F полно и эсэнтически сюржективен, и G — произвольный функтор, то композиция F ⋙ G является добавитивной.

LaTeX

$$[Full F] [EssSurj F] (G : D ⥤ E) [(F ⋙ G).Additive] : G.Additive$$

Lean4

theorem additive_of_full_essSurj_comp [Full F] [EssSurj F] (G : D ⥤ E) [(F ⋙ G).Additive] : G.Additive where
  map_add
    {X Y f
      g} :=
    by
    obtain ⟨f', hf'⟩ := F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
    obtain ⟨g', hg'⟩ := F.map_surjective ((F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv)
    simp only [← cancel_mono (G.map (F.objObjPreimageIso Y).inv), ← cancel_epi (G.map (F.objObjPreimageIso X).hom),
      Preadditive.add_comp, Preadditive.comp_add, ← Functor.map_comp]
    erw [← hf', ← hg', ← (F ⋙ G).map_add]
    dsimp
    rw [F.map_add]

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