independent_iInf_maxGenEigenspace_of_forall_mapsTo

English

There exists an independent iSupIndep family formed from iInf of maxGenEigenspace spaces.

Русский

Существует независимая семейство iSupIndep, образованная пространствами iInf maxGenEigenspace.

LaTeX

$$$$ \text{There exists an independent } iSupIndep(\chi \mapsto \inf_i (f_i).maxGenEigenspace(\chi_i)). $$$$

Lean4

theorem independent_iInf_maxGenEigenspace_of_forall_mapsTo
    (h : ∀ i j φ, MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ)) :
    iSupIndep fun χ : ι → R ↦ ⨅ i, (f i).maxGenEigenspace (χ i) :=
  by
  replace h (l : ι) (χ : ι → R) :
    MapsTo (f l) (⨅ i, (f i).maxGenEigenspace (χ i)) (⨅ i, (f i).maxGenEigenspace (χ i)) :=
    by
    intro x hx
    simp only [iInf_eq_iInter, mem_iInter, SetLike.mem_coe] at hx ⊢
    exact fun i ↦ h l i (χ i) (hx i)
  classical
  suffices
    ∀ χ (s : Finset (ι → R)) (_ : χ ∉ s),
      Disjoint (⨅ i, (f i).maxGenEigenspace (χ i)) (s.sup fun (χ : ι → R) ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
    by
    simpa only [iSupIndep_iff_supIndep_of_injOn (injOn_iInf_maxGenEigenspace f),
      Finset.supIndep_iff_disjoint_erase] using fun s χ _ ↦ this _ _ (s.notMem_erase χ)
  intro χ₁ s
  induction s using Finset.induction_on with
  | empty => simp
  | insert χ₂ s _n ih =>
    intro hχ₁₂
    obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
    specialize ih hχ₁
    rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
    rintro x ⟨hx, hx'⟩
    simp only [SetLike.mem_coe] at hx hx'
    suffices x ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
      by
      rw [← Submodule.mem_bot (R := R), ← (disjoint_iInf_maxGenEigenspace f hχ₁₂).eq_bot]
      exact ⟨hx, this⟩
    obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
    suffices
      ∀ l,
        ∃ (k : ℕ),
          ((f l - algebraMap R (Module.End R M) (χ₂ l)) ^ k) (y + z) ∈
            (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓ Finset.sup s fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
      by simpa [ih.eq_bot, Submodule.mem_bot] using this
    intro l
    let g : Module.End R M := f l - algebraMap R (Module.End R M) (χ₂ l)
    obtain ⟨k, hk : (g ^ k) y = 0⟩ := (mem_iInf_maxGenEigenspace_iff _ _ _).mp hy l
    have aux (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M) (hp : MapsTo f p p) :
      MapsTo ((f - algebraMap R (Module.End R M) φ) ^ k) p p :=
      by
      rw [Module.End.coe_pow]
      exact MapsTo.iterate (fun m hm ↦ p.sub_mem (hp hm) (p.smul_mem _ hm)) k
    refine ⟨k, Submodule.mem_inf.mp ⟨?_, ?_⟩⟩
    · refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ?_ hx
      simp only [Submodule.coe_iInf]
      exact h l χ₁
    · rw [map_add, hk, zero_add]
      suffices
        (s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i))).map (g ^ k) ≤
          s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i))
        from this (Submodule.mem_map_of_mem hz)
      simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := ι → R), Submodule.map_iSup (ι := _ ∈ s)]
      refine iSup₂_mono fun χ _ ↦ ?_
      rintro - ⟨u, hu, rfl⟩
      refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu
      simp only [Submodule.coe_iInf]
      exact h l χ

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