English
For a family e : I → R with all e i idempotent, the Pi-based quotient map is bijective provided certain coprime and product conditions hold.
Русский
Для семейства e : I → R, все e_i идемпотенты, отображение по Pi через фактор-части является биективным при соблюдении условий взаимно простых и произведения.
LaTeX
$$$\\text{pi\_bijective\_of\_isIdempotentElem}(e) :\\; \\text{Bijective} (\\Pi \\;\\text{quotients by } e_i)$$$
Lean4
theorem pi_bijective_of_isIdempotentElem (e : I → R) (he : ∀ i, IsIdempotentElem (e i))
(he₁ : ∀ i j, i ≠ j → (1 - e i) * (1 - e j) = 0) (he₂ : ∏ i, e i = 0) :
Function.Bijective (Pi.ringHom fun i ↦ Ideal.Quotient.mk (Ideal.span {e i})) :=
(CompleteOrthogonalIdempotents.of_prod_one_sub ⟨fun i ↦ (he i).one_sub, he₁⟩ (by simpa using he₂)).bijective_pi'
