map_smul_of_iInf_genEigenspace_ne_bot

English

If the family maps are consistent, then the μ-values scale linearly with t: μ(t·x) = t·μ(x).

Русский

Если вся эта структура допускает линейное изменение μ, то μ(t·x) = t·μ(x).

LaTeX

$$$\\forall t\\in R,\\; \\forall x\\in L,\\; μ(t \\cdot x) = t \\cdot μ(x)$$$

Lean4

theorem map_smul_of_iInf_genEigenspace_ne_bot [NoZeroSMulDivisors R M] {L F : Type*} [SMul R L] [FunLike F L (End R M)]
    [MulActionHomClass F R L (End R M)] (f : F) (μ : L → R) (k : ℕ∞) (h_ne : ⨅ x, (f x).genEigenspace (μ x) k ≠ ⊥)
    (t : R) (x : L) : μ (t • x) = t • μ x := by
  by_contra contra
  let g : L → Submodule R M := fun x ↦ (f x).genEigenspace (μ x) k
  have : ⨅ x, g x ≤ g x ⊓ g (t • x) := le_inf_iff.mpr ⟨iInf_le g x, iInf_le g (t • x)⟩
  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
  apply Disjoint.mono_left (genEigenspace_le_smul (f x) (μ x) t k)
  simp only [g, map_smul]
  exact disjoint_genEigenspace (t • f x) (Ne.symm contra) k k

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