rid — Mathlib

English

The transitive composition of the commutativity and left-identity isomorphisms equals the left-identity; i.e., commuting the left identity across the tensor product yields the left identity.

Русский

Сочетание тождественности слева и коммутативности тензорного произведения эквивалентно левому тождественному отображению.

LaTeX

$$$ (TensorProduct.comm R R M) \\circ (TensorProduct.lid R M) = TensorProduct.lid R M $$$

Lean4

/-- The base ring is a right identity for the tensor product of modules, up to linear equivalence.
-/
protected def rid : M ⊗[R] R ≃ₗ[R] M :=
  LinearEquiv.ofLinear (lift <| .flip (LinearMap.lsmul R M)) (mk R M R |>.flip 1) (LinearMap.ext <| one_smul _)
    (ext <| by ext; simp)

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