English
The span of elements of the form y = hI.dpow n x (with n > 0 and x in S) is contained in I; this is a simplification of dpow_span_isSubideal.
Русский
Образ по форме y = hI.dpow n x (n > 0, x ∈ S) содержится в I; это упрощение dpow_span_isSubideal.
LaTeX
$$There exists a simplified relation proving span ⊆ I under the given hypotheses$$
Lean4
/-- The underlying ideal of `SubDPIdeal.span hI S` is generated by the elements
of the form `hI.dpow n x` with `n > 0` and `x ∈ S`. -/
theorem span_carrier_eq_dpow_span {S : Set A} (hS : S ⊆ I) :
(SubDPIdeal.span hI S).carrier = span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} :=
by
set J : SubDPIdeal hI :=
{ carrier := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
isSubideal := hI.dpow_span_isSubideal hS
dpow_mem _ hk _ hz := dpow_mem_span_of_mem_span hI hS hk hz }
simp only [SubDPIdeal.span, sInf_carrier_def]
apply le_antisymm
· have h : J ∈ insert ⊤ {J : hI.SubDPIdeal | S ⊆ ↑J.carrier} :=
Set.mem_insert_of_mem _ (fun x hx ↦ subset_span ⟨1, one_ne_zero, x, hx, by rw [hI.dpow_one (hS hx)]⟩)
refine sInf_le_of_le ⟨J, ?_⟩ (le_refl _)
simp only [h, ciInf_pos, J]
· rw [le_iInf₂_iff]
intro K hK
have : S ≤ K := by
simp only [Set.mem_insert_iff, Set.mem_setOf_eq] at hK
rcases hK with rfl | hKS
exacts [hS, hKS]
rw [span_le]
rintro y ⟨n, hn, x, hx, rfl⟩
exact K.dpow_mem n hn x (this hx)
