compr₂ — Mathlib

English

Two algebra morphisms from the even subalgebra are equal if they agree on the embedding of the even generators; i.e., ext_lemma for EvenHom.

Русский

Два гомоморфизма поAlgebra из чётной подалгебры равны, если они совпадают на вложении базисных чётных элементов.

LaTeX

$$If (even.ι Q).compr₂ f = (even.ι Q).compr₂ g then f = g$$

Lean4

/-- Compose an `EvenHom` with an `AlgHom` on the output. -/
@[simps]
def compr₂ (g : EvenHom Q A) (f : A →ₐ[R] B) : EvenHom Q B
    where
  bilin := g.bilin.compr₂ f.toLinearMap
  contract _m := (f.congr_arg <| g.contract _).trans <| f.commutes _
  contract_mid _m₁ _m₂
    _m₃ := (map_mul f _ _).symm.trans <| (f.congr_arg <| g.contract_mid _ _ _).trans <| map_smul f _ _

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