English
In a linear topology, the basis inclusion reduces to a conjunction of inclusions on the left ideal J and the index d on the right.
Русский
В линейной топологии базис сводится к союзу включений левой идеал J и правого индекса d.
LaTeX
$$theorem basis_le_iff {J K : TwoSidedIdeal R} {d e : Finsupp σ Nat},
Ne K (TwoSidedIdeal.instTop R).top →
Iff
(CompleteLattice.instOmegaCompletePartialOrder.le (MvPowerSeries.LinearTopology.basis σ R { fst := J, snd := d })
(MvPowerSeries.LinearTopology.basis σ R { fst := K, snd := e }))
(And (CompleteLattice.instOmegaCompletePartialOrder.le J K) (Finsupp.instLE.le e d))$$
Lean4
/-- `basis σ R ⟨J, d⟩ ≤ basis σ R ⟨K, e⟩` if and only if `J ≤ K` and `e ≤ d`. -/
theorem basis_le_iff {J K : TwoSidedIdeal R} {d e : σ →₀ ℕ} (hK : K ≠ ⊤) :
basis σ R ⟨J, d⟩ ≤ basis σ R ⟨K, e⟩ ↔ J ≤ K ∧ e ≤ d := by
classical
constructor
· simp only [basis, TwoSidedIdeal.le_iff, TwoSidedIdeal.coe_mk', setOf_subset_setOf]
intro h
constructor
· intro x hx
have (d' : _) : coeff d' (C (σ := σ) x) ∈ J := by rw [coeff_C]; split_ifs <;> [exact hx; exact J.zero_mem]
simpa using h (C x) (fun _ _ ↦ this _) _ (zero_le _)
· by_contra h'
apply hK
rw [eq_top_iff]
intro x _
have (d') (hd'_le : d' ≤ d) : coeff d' (monomial e x) ∈ J :=
by
rw [coeff_monomial]
split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]
simpa using h (monomial e x) this _ le_rfl
· rintro ⟨hJK, hed⟩
exact basis_le hJK hed
