exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule

English

There exists a subset Φ of indices such that for i ∈ Φ, q is not disjoint from the span of P.root i, while for i ∉ Φ, q ≤ ker (P.coroot' i).

Русский

Существует подмножество Φ индексов такое, что для i ∈ Φ q не пересекается с порождением span(P.root i), а для i ∉ Φ q ≤ ker (P.coroot' i).

LaTeX

$$$$ \exists \Phi \subseteq \iota, \ (\forall i \in \Phi, \ \text{Disjoint}(q, \mathrm{span}_R(P.root_i)) = \text{false}) \wedge (\forall i \notin \Phi, \ q \le \ker (P.coroot'(i))). $$$$

Lean4

theorem exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule [NeZero (2 : R)] [NoZeroSMulDivisors R M]
    (q : Submodule R M) (hq : ∀ i, q ∈ invtSubmodule (P.reflection i)) :
    ∃ Φ : Set ι, (∀ i ∈ Φ, ¬Disjoint q (R ∙ P.root i)) ∧ (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) :=
  by
  refine ⟨{i | ¬Disjoint q (R ∙ P.root i)}, by simp, fun i hi ↦ ?_⟩
  simp only [mem_setOf_eq, not_not] at hi
  rw [← Submodule.mem_invtSubmodule_reflection_iff (by simp) hi]
  exact hq i

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