instFaithfulRestrictScalars — Mathlib

English

Restriction along α is a faithful functor; different morphisms remain different after restriction.

Русский

Ограничение по α сохраняет различие между гомоморфизмами: если их изображения равны после ограничения, то исходные гомоморфизмы равны.

LaTeX

$$$(\\restrictScalars(\\alpha)).Faithful$$$

Lean4

instance (α : R ⟶ R') : (restrictScalars α).Faithful where
  map_injective h := (toPresheaf R').map_injective ((toPresheaf R).congr_map h)

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