bijective_pi' — Mathlib

English

If (1 − e·) is a complete orthogonal idempotents system, then the same Pi map with e replaced by e′ is bijective.

Русский

Если (1 − e·) образует систему, то та же карта Pi с заменой e на e′ тоже биективна.

LaTeX

$$$\\text{CompleteOrthogonalIdempotents } (1 - e\\cdot) \\Rightarrow \\text{Bijective} (\\Pi \\;\\text{quotients by } e_i)$$$

Lean4

theorem bijective_pi' (he : CompleteOrthogonalIdempotents (1 - e ·)) :
    Function.Bijective (Pi.ringHom fun i ↦ Ideal.Quotient.mk (Ideal.span {e i})) :=
  by
  obtain ⟨e', rfl, h⟩ :
    ∃ e' : I → R, (e' = e) ∧ Function.Bijective (Pi.ringHom fun i ↦ Ideal.Quotient.mk (Ideal.span {e' i})) :=
    ⟨_, funext (by simp), he.bijective_pi⟩
  exact h

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