orderIsoMapComap — Mathlib

English

For p, q: Submodule R M, (p.map f ⊔ q.map f).comap f = p ⊔ q.

Русский

Для p и q: подмодули M, обратный образ суммы образов равен сумме подмодулей.

LaTeX

$$$\forall p\, q:\, Submodule\; R\; M,\ (p.map f \sqcup q.map f).comap f = p \sqcup q$$$

Lean4

/-- A linear isomorphism induces an order isomorphism of submodules. -/
@[simps! apply]
def orderIsoMapComap [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) : Submodule R M ≃o Submodule R₂ M₂ :=
  orderIsoMapComapOfBijective f (EquivLike.bijective f)

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