English
The Möbius function respects duality: μ in αᵒᵈ equals μ with swapped arguments in α.
Русский
Функция Мёбиуса сохраняет двойственность: μ в αᵒᵈ равна μ с поменятыми аргументами в α.
LaTeX
$$$ μ 𝕜 (toDual a) (toDual b) = μ 𝕜 b a $$$
Lean4
@[simp]
theorem mu_toDual (a b : α) : mu 𝕜 (toDual a) (toDual b) = mu 𝕜 b a :=
by
letI : DecidableLE α := Classical.decRel _
let mud : IncidenceAlgebra 𝕜 αᵒᵈ :=
{ toFun := fun a b ↦ mu 𝕜 (ofDual b) (ofDual a)
eq_zero_of_not_le' := fun a b hab ↦ apply_eq_zero_of_not_le (by exact hab) _ }
suffices mu 𝕜 = mud by simp_rw [this, mud, coe_mk, ofDual_toDual]
suffices mud * zeta 𝕜 = 1 by
rw [← mu_mul_zeta] at this
apply_fun (· * mu 𝕜) at this
symm
simpa [mul_assoc, zeta_mul_mu] using this
clear a b
ext a b
simp only [mul_boole, one_apply, mul_apply, zeta_apply]
calc
∑ x ∈ Icc a b, (if x ≤ b then mud a x else 0) = ∑ x ∈ Icc a b, mud a x := by congr! with x hx;
exact if_pos (mem_Icc.1 hx).2
_ = ∑ x ∈ Icc (ofDual b) (ofDual a), mu 𝕜 x (ofDual a) := by simp [Icc_orderDual_def, mud]
_ = if ofDual b = ofDual a then 1 else 0 := sum_Icc_mu_left ..
_ = if a = b then 1 else 0 := by simp [eq_comm]
