comap_injective — Mathlib

English

If the star-algebra homomorphism f: A →⋆ₐ[R] B is surjective, then the map S ↦ S.comap f is injective on StarSubalgebras of B.

Русский

Если гомоморфизм f сатурируется на B, то отображение S ↦ S.comap f инъективно на StarSubalgebra(B).

LaTeX

$$If hf : Function.Surjective f, then Function.Injective (StarSubalgebra.comap f).$$

Lean4

theorem comap_injective {f : A →⋆ₐ[R] B} (hf : Function.Surjective f) : Function.Injective (comap f) := fun _S₁ _S₂ h =>
  ext fun b =>
    let ⟨x, hx⟩ := hf b
    let this := SetLike.ext_iff.1 h x
    hx ▸ this

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