exists_smodEq — Mathlib

English

Let pb be a power basis of B over A. Then for every b in B there exists an a in A such that b is congruent to algebraMap_A_B(a) modulo the ideal generated by pb.gen; equivalently, b − algebraMap_A_B(a) lies in the span of pb.gen.

Русский

Пусть pb является базисом мощности для B над A. Тогда для каждого b в B существует a в A such that b эквивалентно algebraMap_A_B(a) по модулю идеала, порождённого pb.gen; эквивалентно, b − algebraMap_A_B(a) принадлежит порождающему(pb.gen) идеалу.

LaTeX

$$$\exists a\in A\; (b - \text{algebraMap}_A^B(a)) \in \operatorname{span}\{ pb.gen \}$$$

Lean4

theorem exists_smodEq (pb : PowerBasis A B) (b : B) : ∃ a, SModEq (Ideal.span ({ pb.gen })) b (algebraMap A B a) :=
  by
  rcases subsingleton_or_nontrivial B
  · exact ⟨0, by rw [SModEq, Subsingleton.eq_zero b, map_zero]⟩
  refine ⟨pb.basis.repr b ⟨0, pb.dim_pos⟩, ?_⟩
  have H := pb.basis.sum_repr b
  rw [← insert_erase (mem_univ ⟨0, pb.dim_pos⟩), sum_insert (notMem_erase _ _)] at H
  rw [SModEq, ← add_zero (algebraMap _ _ _), Quotient.mk_add]
  nth_rewrite 1 [← H]
  rw [Quotient.mk_add]
  congr 1
  · simp [Algebra.algebraMap_eq_smul_one ((pb.basis.repr b) _)]
  · rw [Quotient.mk_zero, Quotient.mk_eq_zero, coe_basis]
    refine sum_mem _ (fun i hi ↦ ?_)
    rw [Algebra.smul_def']
    refine
      Ideal.mul_mem_left _ _ <|
        Ideal.pow_mem_of_mem _ (Ideal.subset_span (by simp)) _ <|
          Nat.pos_of_ne_zero <| fun h ↦ notMem_erase i univ <| Fin.eq_mk_iff_val_eq.2 h ▸ hi

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