English
Compatibility of injections with morphisms: for any f: j ⟶ j' and x ∈ F.obj j, the injection from j' after applying F.map f matches the injection from j before applying x: Quot.ι F j' (F.map f x) = Quot.ι F j x.
Русский
Совместимость инфиксов с отображением: для любого Морфизма f: j ⟶ j' и элемента x ∈ F.obj j выполняется Quot.ι F j' (F.map f x) = Quot.ι F j x.
LaTeX
$$$ \mathrm{Quot}.\mathrm{ι} F j' (F.map f x) = \mathrm{Quot}.\mathrm{ι} F j x $$$
Lean4
@[simp]
theorem map_ι [DecidableEq J] {j j' : J} {f : j ⟶ j'} (x : F.obj j) : Quot.ι F j' (F.map f x) = Quot.ι F j x :=
by
dsimp [ι]
refine eq_of_sub_eq_zero ?_
erw [← (QuotientAddGroup.mk' (Relations F)).map_sub, ← AddMonoidHom.mem_ker]
rw [QuotientAddGroup.ker_mk']
simp only [DFinsupp.singleAddHom_apply]
exact AddSubgroup.subset_closure ⟨j, j', f, x, rfl⟩
