infinite_of_linearIndependent_coxeterWeight_four

English

If two root vectors are linearly independent, one cannot have their Coxeter weight equal to four.

Русский

Если две корневые векторы линейно независимы, их кокетерова вес не может быть равна четырём.

LaTeX

$$$$ \\operatorname{LI}_R(\\![P.root i, P.root j]\\!) \\Rightarrow P.coxeterWeight i j \\neq 4. $$$$

Lean4

theorem infinite_of_linearIndependent_coxeterWeight_four [NeZero (2 : R)] [NoZeroSMulDivisors ℤ M]
    (hl : LinearIndependent R ![P.root i, P.root j]) (hc : P.coxeterWeight i j = 4) : Infinite ι :=
  by
  refine
    (infinite_range_iff (Embedding.injective P.root)).mp
      (Infinite.mono ?_
        ((infinite_range_reflection_reflection_iterate_iff (P.coroot_root_two i) (P.coroot_root_two j) ?_).mpr ?_))
  · rw [range_subset_iff]
    intro n
    rw [←
      IsFixedPt.image_iterate
        ((bijOn_reflection_of_mapsTo (P.coroot_root_two i) (P.mapsTo_reflection_root i)).comp
            (bijOn_reflection_of_mapsTo (P.coroot_root_two j) (P.mapsTo_reflection_root j))).image_eq
        n]
    exact mem_image_of_mem _ (mem_range_self j)
  · rw [coroot_root_eq_pairing, coroot_root_eq_pairing, ← hc, mul_comm, coxeterWeight]
  · rw [LinearIndependent.pair_iff] at hl
    specialize hl (P.pairing j i) (-2)
    simp only [neg_smul, neg_eq_zero, two_ne_zero (α := R), and_false, imp_false] at hl
    rw [ne_eq, coroot_root_eq_pairing, ← sub_eq_zero, sub_eq_add_neg]
    exact hl

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