English
Under the same hypotheses as above, the additivity of G is equivalent to the additivity of L ∘ G.
Русский
При тех же предположениях аддитивность G эквивалентна аддитивности L ∘ G.
LaTeX
$$$G\text{ Additive} \iff (L \circ G)\text{ Additive}$$$
Lean4
theorem functor_additive_iff {E : Type*} [Category E] [Preadditive E] [Preadditive D] [L.Additive] (G : D ⥤ E) :
G.Additive ↔ (L ⋙ G).Additive := by
constructor
· intro
infer_instance
· intro h
suffices ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
by
refine ⟨fun {X Y f g} => ?_⟩
have hL := essSurj L W
have eq :=
this ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv)
((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)
rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp, ← comp_add, ← comp_add, ← add_comp, ←
add_comp, Functor.map_comp, Functor.map_comp] at eq
rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv), ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]
intro X Y f g
obtain ⟨φ, rfl, rfl⟩ := exists_leftFraction₂ L W f g
have := Localization.inverts L W φ.s φ.hs
rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp, add_comp, ← G.map_comp, ←
G.map_comp, LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ←
Functor.comp_map, Functor.map_add, Functor.comp_map, Functor.comp_map]
