English
Given S ⊆ I, the sub-dp-ideal generated by S, i.e., span S, is a sub-dp-ideal of I if and only if for every nonzero n and every s ∈ S, hI.dpow n s ∈ span S.
Русский
Пусть S ⊆ I. Под dp-идеал, порождённый S, то есть span S, является под dp-идеалом I тогда и только тогда, когда для каждого ненулевого n и каждого s ∈ S выполняется hI.dpow n s ∈ span S.
LaTeX
$$IsSubDPIdeal hI (span S) iff ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S$$
Lean4
/-- [P. Berthelot and A. Ogus, *Notes on crystalline cohomology* (Lemma 3.6)][BerthelotOgus-1978] -/
theorem span_isSubDPIdeal_iff {S : Set A} (hS : S ⊆ I) :
IsSubDPIdeal hI (span S) ↔ ∀ {n : ℕ} (_ : n ≠ 0), ∀ s ∈ S, hI.dpow n s ∈ span S :=
by
refine ⟨fun hhI n hn s hs ↦ hhI.dpow_mem n hn (subset_span hs), fun hhI ↦ ?_⟩
· -- interesting direction
have hSI := span_le.mpr hS
apply IsSubDPIdeal.mk hSI
intro m hm z hz
induction hz using Submodule.span_induction generalizing m hm with
| mem x h => exact hhI hm x h
| zero =>
rw [hI.dpow_eval_zero hm]
exact (span S).zero_mem
| add x y hxI hyI hx hy =>
rw [hI.dpow_add' (hSI hxI) (hSI hyI)]
apply Submodule.sum_mem (span S)
intro m _
by_cases hm0 : m = 0
· exact hm0 ▸ mul_mem_left (span S) _ (hy _ hm)
· exact mul_mem_right _ (span S) (hx _ hm0)
| smul a x hxI hx =>
rw [Algebra.id.smul_eq_mul, hI.dpow_mul (hSI hxI)]
exact mul_mem_left (span S) (a ^ m) (hx m hm)
