submodule_eq_span_le_iff_stable_ge

English

For any n0, if F.submodule equals the span of i ≤ n0, then for all n ≥ n0 we have the stabilization condition I • F.N(n) = F.N(n+1); the converse also holds.

Русский

Для любого n0, равенство F.submodule span-условия означает стабилизацию: I • F.N(n) = F.N(n+1) для всех n ≥ n0, и наоборот.

LaTeX

$$$F.submodule = \\operatorname{span} (\\bigcup_{i ≤ n_0} \\mathrm{single}_R(i) '' (F.N(i) : Set M)) \\iff \\forall n ≥ n_0,\\ I \\cdot F.N(n) = F.N(n+1).$$$

Lean4

theorem submodule_eq_span_le_iff_stable_ge (n₀ : ℕ) :
    F.submodule = Submodule.span _ (⋃ i ≤ n₀, single R i '' (F.N i : Set M)) ↔ ∀ n ≥ n₀, I • F.N n = F.N (n + 1) :=
  by
  rw [← submodule_span_single, ← (Submodule.span_mono (Set.iUnion₂_subset_iUnion _ _)).ge_iff_eq', Submodule.span_le,
    Set.iUnion_subset_iff]
  constructor
  · intro H n hn
    refine (F.smul_le n).antisymm ?_
    intro x hx
    obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp (H _ ⟨x, hx, rfl⟩)
    replace hl := congr_arg (fun f : ℕ →₀ M => f (n + 1)) hl
    dsimp only at hl
    rw [PolynomialModule.single_apply, if_pos rfl] at hl
    rw [← hl, Finsupp.linearCombination_apply, Finsupp.sum_apply]
    apply Submodule.sum_mem _ _
    rintro ⟨_, _, ⟨n', rfl⟩, _, ⟨hn', rfl⟩, m, hm, rfl⟩ -
    dsimp only [Subtype.coe_mk]
    rw [Subalgebra.smul_def, smul_single_apply, if_pos (show n' ≤ n + 1 by cutsat)]
    have e : n' ≤ n := by omega
    have := F.pow_smul_le_pow_smul (n - n') n' 1
    rw [tsub_add_cancel_of_le e, pow_one, add_comm _ 1, ← add_tsub_assoc_of_le e, add_comm] at this
    exact this (Submodule.smul_mem_smul ((l _).2 <| n + 1 - n') hm)
  · let F' := Submodule.span (reesAlgebra I) (⋃ i ≤ n₀, single R i '' (F.N i : Set M))
    intro hF i
    have : ∀ i ≤ n₀, single R i '' (F.N i : Set M) ⊆ F' :=
      fun i hi =>
        -- Porting note: need to add hint for `s`

      (Set.subset_iUnion₂ (s := fun i _ => (single R i '' (N F i : Set M))) i hi).trans Submodule.subset_span
    induction i with
    | zero => exact this _ (zero_le _)
    | succ j hj => ?_
    by_cases hj' : j.succ ≤ n₀
    · exact this _ hj'
    simp only [not_le, Nat.lt_succ_iff] at hj'
    rw [← hF _ hj']
    rintro _ ⟨m, hm, rfl⟩
    refine Submodule.smul_induction_on hm (fun r hr m' hm' => ?_) (fun x y hx hy => ?_)
    · rw [add_comm, ← monomial_smul_single]
      exact F'.smul_mem ⟨_, reesAlgebra.monomial_mem.mpr (by rwa [pow_one])⟩ (hj <| Set.mem_image_of_mem _ hm')
    · rw [map_add]
      exact F'.add_mem hx hy

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