map_comap_incl — Mathlib

English

For LieSubmodules N,N' of M, the image of the pullback of N' along the inclusion N.incl equals the intersection N ∩ N'.

Русский

Для подмодулов Ли N и N' подмодуль изображения композиции включения N.incl скомпоновавшейся с прообразом N' даёт пересечение N ∩ N'.

LaTeX

$$$$\mathrm{map}\,N.\incl\big(\mathrm{comap}\,N.\incl\,N'\big) = N \cap N'. $$$$

Lean4

@[simp]
theorem map_comap_incl : map N.incl (comap N.incl N') = N ⊓ N' :=
  by
  rw [← toSubmodule_inj]
  exact (N : Submodule R M).map_comap_subtype N'

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