ofHom₂_compr₂ — Mathlib

English

Let f: M ⇢ N ⇢ P and g: P ⇢ Q be linear maps. Then the two-variable lifting satisfies ofHom₂ (f.compr₂ g) = ofHom₂ f ≫ ofHom (Linear.rightComp R _ (ofHom g)).

Русский

Пусть f: M → N → P и g: P → Q — линейные отображения. Тогда связанный с ними подстановочный lift удовлетворяет равенству ofHom₂ (f.compr₂ g) = ofHom₂ f ≫ ofHom (Linear.rightComp R _ (ofHom g)).

LaTeX

$$$\\text{ofHom}_2 (f.\\text{compr}_2 g) = \\text{ofHom}_2 f \\;\\;\\circ\\; \\text{ofHom} (\\text{Linear.rightComp } R \\; \\_ (\\text{ofHom } g))$$$

Lean4

@[simp]
theorem ofHom₂_compr₂ {M N P Q : ModuleCat.{u} R} (f : M →ₗ[R] N →ₗ[R] P) (g : P →ₗ[R] Q) :
    ofHom₂ (f.compr₂ g) = ofHom₂ f ≫ ofHom (Linear.rightComp R _ (ofHom g)) :=
  rfl

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