English
A collection of orthogonal idempotents e : I → R yields a surjective map from R to the product of quotients by (1 − e i).
Русский
Множество ортогональных идемпотентов e : I → R задает сюрьективное отображение из R в произведение частичных факторизаций по (1 − e_i).
LaTeX
$$$\\forall e : I \\to R,\\; OrthogonalIdempotents e \\Rightarrow \\\\text{Surjective} \\Big( Pi.ringHom (i \\mapsto \\mathrm{Ideal}.Quotient.mk (\\mathrm{Ideal}.span {1 - e i})) \\Big)$$$
Lean4
/-- A family of orthogonal idempotents induces an surjection `R ≃+* ∏ R ⧸ ⟨1 - eᵢ⟩` -/
theorem surjective_pi {I : Type*} [Finite I] {e : I → R} (he : OrthogonalIdempotents e) :
Function.Surjective (Pi.ringHom fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) :=
by
suffices Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
by
intro x
obtain ⟨x, rfl⟩ := Ideal.quotientInfToPiQuotient_surj this x
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
exact ⟨x, by ext i; simp [Ideal.quotientInfToPiQuotient]⟩
intro i j hij
rw [Ideal.isCoprime_span_singleton_iff]
exact ⟨1, e i, by simp [mul_sub, he.ortho hij]⟩
