English
All polynomials are in the span of the range of S if each leadingCoeff is a unit; i.e., span of Set.range S equals top.
Русский
Если все ведущие коэффициенты единицы по модулю, то каждый полином лежит в линейном замкнутом span(S).
LaTeX
$$$\forall S, \Big(\forall i, IsUnit (S i).leadingCoeff\Big) \Rightarrow \operatorname{span} R (\operatorname{Set.range} S) = \top$$$
Lean4
/-- A polynomial sequence spans `R[X]` if all of its elements' leading coefficients are units. -/
protected theorem span (hCoeff : ∀ i, IsUnit (S i).leadingCoeff) : span R (Set.range S) = ⊤ :=
by
rw [eq_top_iff']
intro P
nontriviality R using Subsingleton.eq_zero P
generalize hp : P.natDegree = n
induction n using Nat.strong_induction_on generalizing P with
| h n ih =>
by_cases p_ne_zero : P = 0
·
simp [p_ne_zero]
-- let u be the inverse of `S n`'s leading coefficient
obtain ⟨u, leftinv, rightinv⟩ := isUnit_iff_exists.mp <| hCoeff n
let head := P.leadingCoeff • u • S n
let tail := P - head
have head_mem_span : head ∈ span R (Set.range S) :=
by
have in_span : S n ∈ span R (Set.range S) := subset_span (by simp)
have smul_span := smul_mem (span R (Set.range S)) (P.leadingCoeff • u) in_span
rwa [smul_assoc] at smul_span
by_cases tail_eq_zero : tail = 0
·
simp [head_mem_span, sub_eq_iff_eq_add.mp tail_eq_zero]
-- we'll do so via the induction hypothesis,
-- and once we show we can use it, `P` is a difference of two members of the span
refine
sub_mem_iff_left _ head_mem_span |>.mp <|
-- so let's prove the tail has degree less than `n`
ih tail.natDegree (natDegree_lt_iff_degree_lt tail_eq_zero |>.mpr ?_) _ rfl
have isRightRegular_smul_leadingCoeff : IsRightRegular (u • S n).leadingCoeff := by
simpa [leadingCoeff_smul_of_smul_regular, IsSMulRegular.of_mul_eq_one leftinv, rightinv] using isRegular_one.right
have u_degree_same :=
degree_smul_of_isRightRegular_leadingCoeff (left_ne_zero_of_mul_eq_one rightinv) (hCoeff n).isRegular.right
have head_degree_eq :=
degree_smul_of_isRightRegular_leadingCoeff (leadingCoeff_ne_zero.mpr p_ne_zero) isRightRegular_smul_leadingCoeff
rw [u_degree_same, S.degree_eq n, ← hp, eq_comm, ← degree_eq_natDegree p_ne_zero, hp] at head_degree_eq
have head_degree_eq_natDegree : head.degree = head.natDegree :=
degree_eq_natDegree <| by
by_cases n_eq_zero : n = 0
· dsimp [head]
rw [n_eq_zero, ← coeff_natDegree, natDegree_eq] at rightinv
rwa [n_eq_zero, eq_C_of_natDegree_eq_zero <| S.natDegree_eq 0, smul_C, smul_eq_mul, map_mul, ← C_mul,
rightinv, smul_C, smul_eq_mul, mul_one, C_eq_zero, leadingCoeff_eq_zero]
· apply head.ne_zero_of_degree_gt
rw [← head_degree_eq]
exact
natDegree_pos_iff_degree_pos.mp
(by cutsat)
-- and that they have matching leading coefficients
have hPhead : P.leadingCoeff = head.leadingCoeff :=
by
rw [degree_eq_natDegree, head_degree_eq_natDegree] at head_degree_eq
nth_rw 2 [← coeff_natDegree]
rw_mod_cast [← head_degree_eq, hp]
dsimp [head]
nth_rw 2 [← S.natDegree_eq n]
rwa [coeff_smul, coeff_smul, coeff_natDegree, smul_eq_mul, smul_eq_mul, rightinv, mul_one]
-- which we can now combine to show that `P - head` must have strictly lower degree,
-- as its leading term has been cancelled, completing our proof.
have tail_degree_lt := P.degree_sub_lt head_degree_eq p_ne_zero hPhead
rwa [degree_eq_natDegree p_ne_zero, hp] at tail_degree_lt
