comap_bracket_incl — Mathlib

English

If I1 ≤ I and I2 ≤ I for some LieIdeal I in L, then the equality holds: [comap I.incl I1, comap I.incl I2] = comap I.incl [I1, I2].

Русский

Если I1 ≤ I и I2 ≤ I для некоторого I, тогда выполняется равенство: [comap I.incl I1, comap I.incl I2] = comap I.incl [I1, I2].

LaTeX

$$$$ [\operatorname{comap} (I.incl) I_1, \operatorname{comap} (I.incl) I_2] = \operatorname{comap} (I.incl) [I_1, I_2]. $$$$

Lean4

theorem comap_bracket_incl {I₁ I₂ : LieIdeal R L} :
    ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ :=
  by
  conv_rhs =>
    congr
    next => skip
    rw [← I.incl_idealRange]
  rw [comap_bracket_eq]
  · simp only [ker_incl, sup_bot_eq]
  · exact I.incl_isIdealMorphism

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