span_eq_top_of_span_image_evalRingHom

English

If a finite set s in the product ∏ i R_i generates the unit ideal after projecting to each factor i, then the span of s in the full product is the unit ideal.

Русский

Если для каждого i проекция s_i порождает единичную идеал, то общий порождающий идеал от s в произведении равен единице.

LaTeX

$$Let s ⊂ ∏_i R_i be finite. If ∀ i, span(Pi.evalRingHom i '' s) = ⊤, then span s = ⊤.$$

Lean4

theorem span_eq_top_of_span_image_evalRingHom {ι} {R : ι → Type*} [∀ i, CommRing (R i)] (s : Set (Π i, R i))
    (hs : s.Finite) (hs' : ∀ i, Ideal.span (Pi.evalRingHom (R ·) i '' s) = ⊤) : Ideal.span s = ⊤ :=
  by
  simp only [Ideal.eq_top_iff_one, ← Subtype.range_val (s := s), ← Set.range_comp,
    Finsupp.mem_ideal_span_range_iff_exists_finsupp] at hs' ⊢
  choose f hf using hs'
  have : Fintype s := hs.fintype
  refine ⟨Finsupp.equivFunOnFinite.symm fun i x ↦ f x i, ?_⟩
  ext i
  simpa [Finsupp.sum_fintype] using hf i

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