English
A key lemma relating Jacobson-type kernels in the Gabriel–Popescu setup, linking a d-map to a sum formula over finite subcoproducts.
Русский
Ключевая лемма Габриэль-Попеску, связывающая ядра и сумму по конечным подкопродуктам.
LaTeX
$$$\\text{kernel.ι}(d g) \\;\\text{and}\\; d f$ interact via a finite subproduct identity$$
Lean4
/-- This is the "Lemma" in [mitchell1981]. -/
theorem kernel_ι_d_comp_d {G : C} (hG : IsSeparator G) {A B : C} {M : ModuleCat (End G)ᵐᵒᵖ}
(g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) (hg : Mono g) (f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) :
kernel.ι (d g) ≫ d f = 0 :=
by
refine (isColimitFiniteSubproductsCocone (fun (_ : M) => G)).pullback_zero_ext (fun F => ?_)
dsimp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt, Functor.const_obj_obj]
classical
rw [finiteSubcoproductsCocone_ι_app_eq_sum, ← pullback.condition_assoc]
refine (Preadditive.isSeparator_iff G).1 hG _ (fun h => ?_)
rw [Preadditive.comp_sum_assoc, Preadditive.comp_sum_assoc, Preadditive.sum_comp]
simp only [Category.assoc, ι_d]
let r (x : F) : (End G)ᵐᵒᵖ := MulOpposite.op (h ≫ pullback.fst _ _ ≫ Sigma.π _ x)
suffices ∑ x ∈ F.attach, r x • f.hom x.1.as = 0 by simpa [End.smul_left, r] using this
simp only [← LinearMap.map_smul, ← map_sum]
suffices ∑ x ∈ F.attach, r x • x.1.as = 0 by simp [this]
simp only [← g.hom.map_eq_zero_iff ((ModuleCat.mono_iff_injective _).1 hg), map_sum, map_smul]
simp only [← ι_d g, End.smul_left, MulOpposite.unop_op, Category.assoc, r]
simp [← Preadditive.comp_sum, ← Preadditive.sum_comp', pullback.condition_assoc]
