bijective_pi — Mathlib

English

There is a bijection between a complete orthogonal idempotent system and a product of quotient rings by (1 − e_i) via a ring homomorphism.

Русский

Существует биекция между полной ортогональной системой идемпотентов и произведением фактор-гомоморфизмов по (1 − e_i).

LaTeX

$$$\\text{bijective\_pi} = \\text{CompleteOrthogonalIdempotents e} \\Rightarrow \\text{Bijective} (\\Pi \\;\\text{quotients})$$$

Lean4

/-- A family of complete orthogonal idempotents induces an isomorphism `R ≃+* ∏ R ⧸ ⟨1 - eᵢ⟩` -/
theorem bijective_pi (he : CompleteOrthogonalIdempotents e) :
    Function.Bijective (Pi.ringHom fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) := by
  classical
  refine ⟨?_, he.1.surjective_pi⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  simp [funext_iff, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton] at hx
  suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by rw [← this Finset.univ, he.prod_one_sub, zero_mul]
  refine fun s ↦ Finset.induction_on s (by simp) ?_
  intro a s has e'
  suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
  obtain ⟨c, rfl⟩ := hx a
  rw [← mul_assoc, (he.idem a).one_sub.eq]

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