English
The pi bijection result persists under ring homomorphism settings and is preserved by composition with the quotient maps.
Русский
Результат биективной карты Pi сохраняется при условиях гомоморфизмов колец и сохраняется композициями с фактор-маршрутизаторами.
LaTeX
$$$\\text{RingHom.pi\_bijective\_of\_isIdempotentElem}(e) = \\text{bijection}$$$
Lean4
theorem prod_bijective_of_isIdempotentElem {e f : R} (he : IsIdempotentElem e) (hf : IsIdempotentElem f)
(hef₁ : e + f = 1) (hef₂ : e * f = 0) :
Function.Bijective ((Ideal.Quotient.mk <| Ideal.span { e }).prod (Ideal.Quotient.mk <| Ideal.span { f })) :=
by
let o (i : Fin 2) : R :=
match i with
| 0 => e
| 1 => f
change Function.Bijective (piFinTwoEquiv _ ∘ Pi.ringHom (fun i : Fin 2 ↦ Ideal.Quotient.mk (Ideal.span {o i})))
rw [(Equiv.bijective _).of_comp_iff']
apply pi_bijective_of_isIdempotentElem
· intro i
fin_cases i <;> simpa [o]
· intro i j hij
fin_cases i <;> fin_cases j <;> simp at hij ⊢ <;> simp [o, mul_comm, hef₂, ← hef₁]
· simpa
