orderIsoMapComapOfBijective — Mathlib

English

For indexed S : ι → Submodule R M, (⨆ i, (S i).map f).comap f = iSup S.

Русский

Для индексов S: ι → Submodule R M выполняется: обобщение образов, затем обратный образ, равен сумме по индексу.

LaTeX

$$$\forall {\iota : Sort*} (S : ι → Submodule R M), (⨆ i, (S i).map f).comap f = iSup S$$

Lean4

/-- A linear isomorphism induces an order isomorphism of submodules. -/
@[simps symm_apply apply]
def orderIsoMapComapOfBijective [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (hf : Bijective f) :
    Submodule R M ≃o Submodule R₂ M₂ where
  toFun := map f
  invFun := comap f
  left_inv := comap_map_eq_of_injective hf.injective
  right_inv := map_comap_eq_of_surjective hf.surjective
  map_rel_iff' := map_le_map_iff_of_injective hf.injective _ _

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