hom_ext — Mathlib

English

Technical lemma about how lift interacts with composition of algebra maps in the construction of lift equivalence.

Русский

Техническая вспомогательная лемма о том, как lift взаимодействует с композициями алгебра-гомоморфизмов в конструкции эквивалентности.

LaTeX

$$$\\text{(proof}_{1})$$$

Lean4

/-- Two `R`-algebra morphisms from a quaternion algebra are equal if they agree on `i` and `j`. -/
@[ext]
theorem hom_ext ⦃f g : ℍ[R,c₁,c₂,c₃] →ₐ[R] A⦄ (hi : f (Basis.self R).i = g (Basis.self R).i)
    (hj : f (Basis.self R).j = g (Basis.self R).j) : f = g :=
  lift.symm.injective <| Basis.ext hi hj

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