toSubmodule — Mathlib

English

The forgetful map from Subalgebra to Submodule is an order-embedding.

Русский

Отображение от Subalgebra к Submodule является внедрением порядка.

LaTeX

$$$$ \\text{toSubmodule} : \\text{Subalgebra } R A \\hookrightarrow \\text{Submodule } R A $$$$

Lean4

/-- The forgetful map from `Subalgebra` to `Submodule` as an `OrderEmbedding` -/
def toSubmodule : Subalgebra R A ↪o Submodule R A
    where
  toEmbedding :=
    { toFun := fun S =>
        { S with
          carrier := S
          smul_mem' := fun c {x} hx ↦ (Algebra.smul_def c x).symm ▸ mul_mem (S.range_le ⟨c, rfl⟩) hx }
      inj' := fun _ _ h ↦ ext fun x ↦ SetLike.ext_iff.mp h x }
  map_rel_iff' := SetLike.coe_subset_coe.symm.trans SetLike.coe_subset_coe

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