algebraMapSubmonoid_map_eq — Mathlib

English

For any algebra hom f: A →ₐ[R] B and any submonoid M of R, the image of algebraMapSubmonoid A M under f equals algebraMapSubmonoid B M.

Русский

Для любого гомоморфизма f: A →ₐ[R] B и любого подменоида M ⊆ R выполняется равенство: map(algebraMapSubmonoid A M) f = algebraMapSubmonoid B M.

LaTeX

$$$ (algebraMapSubmonoid A M).map\\; f = algebraMapSubmonoid B M $$$

Lean4

theorem algebraMapSubmonoid_map_eq (f : A →ₐ[R] B) : (algebraMapSubmonoid A M).map f = algebraMapSubmonoid B M :=
  by
  ext x
  constructor
  · rintro ⟨a, ⟨r, hr, rfl⟩, rfl⟩
    simp only [AlgHom.commutes]
    use r
  · rintro ⟨r, hr, rfl⟩
    simp only [Submonoid.mem_map]
    use (algebraMap R A r)
    simp only [AlgHom.commutes, and_true]
    use r

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