adjoin_le_equalizer

Mathlib.Algebra.Algebra.Subalgebra.Lattice

URI: https://scilib.ai/kg/mathlib#AlgHom.adjoin_le_equalizer

English

Let S = adjoin_R s. Then two AlgHoms φ₁, φ₂: S → B are equal if they agree on s.

Русский

Пусть S = adjoin_R s. Тогда две AlgHom φ₁, φ₂: S → B равны, если они сходятся на s.

LaTeX

$$$\\text{EqOn }(φ_1,φ_2,s) \\Rightarrow φ_1 = φ_2$ (on S via hS.ge)$$

Lean4

theorem adjoin_le_equalizer (φ₁ φ₂ : A →ₐ[R] B) {s : Set A} (h : s.EqOn φ₁ φ₂) : adjoin R s ≤ equalizer φ₁ φ₂ :=
  adjoin_le h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru