isSeparator — Mathlib

English

If R is small, the module category has a separator object given by ModuleCat.of R (Shrink R).

Русский

Если R мал, категория модулей имеет разделитель, задаваемый модулем ModuleCat.of R (Shrink R).

LaTeX

$$$\operatorname{IsSeparator}(\mathrm{ModuleCat.of}(R, \mathrm{Shrink}(R)))$$$

Lean4

theorem isSeparator [Small.{v} R] : IsSeparator (ModuleCat.of.{v} R (Shrink.{v} R)) := fun X Y f g h ↦
  by
  simp only [Set.mem_singleton_iff, forall_eq, ModuleCat.hom_ext_iff, LinearMap.ext_iff] at h
  ext x
  simpa [Shrink.linearEquiv, Equiv.linearEquiv] using
    h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp (Shrink.linearEquiv R R : Shrink R →ₗ[R] R))) 1

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