English
Euler characteristic equals the evaluation of Möbius on bottom and top: eulerChar 𝕜 α = μ 𝕜 ⊥ ⊤.
Русский
Эйлерова характеристика равна значению функции Мёбиуса на нижней и верхней границе: eulerChar 𝕜 α = μ 𝕜 ⊥ ⊤.
LaTeX
$$$ \text{eulerChar } 𝕜 α = μ 𝕜 (\bot) (\top) $$$
Lean4
/-- A general form of Möbius inversion. Based on lemma 2.1.2 of Incidence Algebras by Spiegel and
O'Donnell. -/
theorem moebius_inversion_top (f g : α → 𝕜) (h : ∀ x, g x = ∑ y ∈ Ici x, f y) (x : α) :
f x = ∑ y ∈ Ici x, mu 𝕜 x y * g y :=
by
letI : DecidableLE α := Classical.decRel _
symm
calc
∑ y ∈ Ici x, mu 𝕜 x y * g y = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, f z := by simp_rw [h]
_ = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, zeta 𝕜 y z * f z :=
by
congr with y
rw [sum_congr rfl fun z hz ↦ ?_]
rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
_ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
_ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z :=
by
rw [sum_sigma' (Ici x) fun y ↦ Ici y]
rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
simp only [mul_boole, zero_mul, ite_mul, zeta_apply]
apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;> aesop (add simp mul_assoc) (add unsafe le_trans)
_ = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by simp_rw [mul_apply, sum_mul]
_ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z :=
by
simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl, ↓reduceIte,
← add_sum_Ioi_eq_sum_Ici, left_eq_add]
exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
_ = f x :=
by
simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, ← add_sum_Ioi_eq_sum_Ici, le_refl,
↓reduceIte, add_eq_left]
exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
