map_comap_incl — Mathlib

English

For Lie ideals I1, I2 in L, the map of comap along the inclusion I1.incl gives the intersection: map I1.incl (comap I1.incl I2) = I1 ∩ I2.

Русский

Для Ли-идеалов I1, I2 в L отображение через включение I1.incl от компарапа даёт пересечение: map I1.incl (comap I1.incl I2) = I1 ∩ I2.

LaTeX

$$$$ \operatorname{map}(\iota_{I_1})(\operatorname{comap}(\iota_{I_1}) I_2) = I_1 \cap I_2. $$$$

Lean4

theorem map_comap_incl {I₁ I₂ : LieIdeal R L} : map I₁.incl (comap I₁.incl I₂) = I₁ ⊓ I₂ :=
  by
  conv_rhs => rw [← I₁.incl_idealRange]
  rw [← map_comap_eq]
  exact I₁.incl_isIdealMorphism

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