includeRight — Mathlib

English

Includes the right factor in a tensor-product setting while preserving the property P via CodescendsAlong.

Русский

Включает правый фактор в настройке тензорного произведения и сохраняет свойство P через CodescendsAlong.

LaTeX

$$$\text{includeRight}(hPQ,h,Q,H) : P(algebraMap R S)$. $$

Lean4

theorem includeRight (hPQ : CodescendsAlong P Q) (h : Q (algebraMap R T))
    (H : P ((Algebra.TensorProduct.includeRight.toRingHom : T →+* S ⊗[R] T))) : P (algebraMap R S) :=
  by
  let _ : Algebra T (S ⊗[R] T) := Algebra.TensorProduct.rightAlgebra
  apply hPQ R S T (S ⊗[R] T) h H

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