Incidence algebras

Given a locally finite order α the incidence algebra over α is the type of functions from non-empty intervals of α to some algebraic codomain.

This algebra has a natural multiplication operation whereby the product of two such functions is defined on an interval by summing over all divisions into two subintervals the product of the values of the original pair of functions.

This structure allows us to interpret many natural invariants of the intervals (such as their cardinality) as elements of the incidence algebra. For instance the cardinality function, viewed as an element of the incidence algebra, is simply the square of the function that takes constant value one on all intervals. This constant function is called the zeta function, after its connection with the Riemann zeta function.

The incidence algebra is a good setting for proving many inclusion-exclusion type principles, these go under the name Möbius inversion, and are essentially due to the fact that the zeta function has a multiplicative inverse in the incidence algebra, an inductively definable function called the Möbius function that generalizes the Möbius function in number theory.

Main definitions

• 1 : IncidenceAlgebra 𝕜 α is the delta function, defined analogously to the identity matrix.
• f * g is the incidence algebra product, defined analogously to the matrix product.
• IncidenceAlgebra.zeta is the zeta function, defined analogously to the upper triangular matrix of ones.
• IncidenceAlgebra.mu is the inverse of the zeta function.

Implementation notes

One has to define mu as either the left or right inverse of zeta. We define it as the left inverse, and prove it is also a right inverse by defining mu' as the right inverse and using that left and right inverses agree if they exist.

TODOs

Here are some additions to this file that could be made in the future:

• Generalize the construction of mu to invert any element of the incidence algebra f which has f x x a unit for all x.
• Give formulas for higher powers of zeta.
• A formula for the möbius function on a pi type similar to the one for products
• More examples / applications to different posets.
• Connection with Galois insertions
• Finsum version of Möbius inversion that holds even when an order doesn't have top/bot?
• Connect this theory to (infinite) matrices, giving maps of the incidence algebra to matrix rings
• Connect to the more advanced theory of arithmetic functions, and Dirichlet convolution.

References

• [Aigner, Combinatorial Theory, Chapter IV][aigner1997]
• [Jacobson, Basic Algebra I, 8.6][jacobson1974]
• [Doubilet, Rota, Stanley, On the foundations of Combinatorial Theory VI][doubilet_rota_stanley_vi]
• [Spiegel, O'Donnell, Incidence Algebras][spiegel_odonnel1997]
• [Kung, Rota, Yan, Combinatorics: The Rota Way, Chapter 3][kung_rota_yan2009]

structure IncidenceAlgebra (𝕜 : Type u_7) (α : Type u_8) [Zero 𝕜] [LE α] : Type (max u_7 u_8)

The 𝕜-incidence algebra over α.

• toFun : α → α → 𝕜

  The underlying function of an element of the incidence algebra.

  Do not use this function directly. Instead use the coercion coming from the FunLike instance.

• eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → self.toFun a b = 0

instance IncidenceAlgebra.instFunLike {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] : FunLike (IncidenceAlgebra 𝕜 α) α (α → 𝕜)

Equations

• IncidenceAlgebra.instFunLike = { coe := IncidenceAlgebra.toFun, coe_injective' := ⋯ }

theorem IncidenceAlgebra.apply_eq_zero_of_not_le {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] {a b : α} (h : ¬a ≤ b) (f : IncidenceAlgebra 𝕜 α) : f a b = 0

theorem IncidenceAlgebra.le_of_ne_zero {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] {a b : α} {f : IncidenceAlgebra 𝕜 α} : f a b ≠ 0 → a ≤ b

@[simp]

theorem IncidenceAlgebra.toFun_eq_coe {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] (f : IncidenceAlgebra 𝕜 α) : f.toFun = ⇑f

@[simp]

theorem IncidenceAlgebra.coe_mk {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] (f : α → α → 𝕜) (h : ∀ ⦃a b : α⦄, ¬a ≤ b → f a b = 0) : ⇑{ toFun := f, eq_zero_of_not_le' := h } = f

theorem IncidenceAlgebra.coe_inj {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] {f g : IncidenceAlgebra 𝕜 α} : ⇑f = ⇑g ↔ f = g

theorem IncidenceAlgebra.ext {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] ⦃f g : IncidenceAlgebra 𝕜 α⦄ (h : ∀ (a b : α), a ≤ b → f a b = g a b) : f = g

@[simp]

theorem IncidenceAlgebra.mk_coe {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] (f : IncidenceAlgebra 𝕜 α) (h : ∀ ⦃a b : α⦄, ¬a ≤ b → f a b = 0) : { toFun := ⇑f, eq_zero_of_not_le' := h } = f

Additive and multiplicative structure

instance IncidenceAlgebra.instZero {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] : Zero (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instZero = { zero := { toFun := fun (x x : α) => 0, eq_zero_of_not_le' := ⋯ } }

instance IncidenceAlgebra.instInhabited {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] : Inhabited (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instInhabited = { default := 0 }

@[simp]

theorem IncidenceAlgebra.coe_zero {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] : ⇑0 = 0

theorem IncidenceAlgebra.zero_apply {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [LE α] (a b : α) : 0 a b = 0

instance IncidenceAlgebra.instAdd {𝕜 : Type u_2} {α : Type u_5} [AddZeroClass 𝕜] [LE α] : Add (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instAdd = { add := fun (f g : IncidenceAlgebra 𝕜 α) => { toFun := ⇑f + ⇑g, eq_zero_of_not_le' := ⋯ } }

@[simp]

theorem IncidenceAlgebra.coe_add {𝕜 : Type u_2} {α : Type u_5} [AddZeroClass 𝕜] [LE α] (f g : IncidenceAlgebra 𝕜 α) : ⇑(f + g) = ⇑f + ⇑g

theorem IncidenceAlgebra.add_apply {𝕜 : Type u_2} {α : Type u_5} [AddZeroClass 𝕜] [LE α] (f g : IncidenceAlgebra 𝕜 α) (a b : α) : (f + g) a b = f a b + g a b

instance IncidenceAlgebra.instSmulZeroClassRight {𝕜 : Type u_2} {α : Type u_5} {M : Type u_7} [Zero 𝕜] [LE α] [SMulZeroClass M 𝕜] : SMulZeroClass M (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instSmulZeroClassRight = SMulZeroClass.mk ⋯

@[simp]

theorem IncidenceAlgebra.coe_constSMul {𝕜 : Type u_2} {α : Type u_5} {M : Type u_7} [Zero 𝕜] [LE α] [SMulZeroClass M 𝕜] (c : M) (f : IncidenceAlgebra 𝕜 α) : ⇑(c • f) = c • ⇑f

theorem IncidenceAlgebra.constSMul_apply {𝕜 : Type u_2} {α : Type u_5} {M : Type u_7} [Zero 𝕜] [LE α] [SMulZeroClass M 𝕜] (c : M) (f : IncidenceAlgebra 𝕜 α) (a b : α) : (c • f) a b = c • f a b

instance IncidenceAlgebra.instAddMonoid {𝕜 : Type u_2} {α : Type u_5} [AddMonoid 𝕜] [LE α] : AddMonoid (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instAddMonoid = Function.Injective.addMonoid (fun (f : IncidenceAlgebra 𝕜 α) => ⇑f) ⋯ ⋯ ⋯ ⋯

instance IncidenceAlgebra.instAddCommMonoid {𝕜 : Type u_2} {α : Type u_5} [AddCommMonoid 𝕜] [LE α] : AddCommMonoid (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instAddCommMonoid = Function.Injective.addCommMonoid (fun (f : IncidenceAlgebra 𝕜 α) => ⇑f) ⋯ ⋯ ⋯ ⋯

instance IncidenceAlgebra.instNeg {𝕜 : Type u_2} {α : Type u_5} [AddGroup 𝕜] [LE α] : Neg (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instNeg = { neg := fun (f : IncidenceAlgebra 𝕜 α) => { toFun := -⇑f, eq_zero_of_not_le' := ⋯ } }

instance IncidenceAlgebra.instSub {𝕜 : Type u_2} {α : Type u_5} [AddGroup 𝕜] [LE α] : Sub (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instSub = { sub := fun (f g : IncidenceAlgebra 𝕜 α) => { toFun := ⇑f - ⇑g, eq_zero_of_not_le' := ⋯ } }

@[simp]

theorem IncidenceAlgebra.coe_neg {𝕜 : Type u_2} {α : Type u_5} [AddGroup 𝕜] [LE α] (f : IncidenceAlgebra 𝕜 α) : ⇑(-f) = -⇑f

@[simp]

theorem IncidenceAlgebra.coe_sub {𝕜 : Type u_2} {α : Type u_5} [AddGroup 𝕜] [LE α] (f g : IncidenceAlgebra 𝕜 α) : ⇑(f - g) = ⇑f - ⇑g

theorem IncidenceAlgebra.neg_apply {𝕜 : Type u_2} {α : Type u_5} [AddGroup 𝕜] [LE α] (f : IncidenceAlgebra 𝕜 α) (a b : α) : (-f) a b = -f a b

theorem IncidenceAlgebra.sub_apply {𝕜 : Type u_2} {α : Type u_5} [AddGroup 𝕜] [LE α] (f g : IncidenceAlgebra 𝕜 α) (a b : α) : (f - g) a b = f a b - g a b

instance IncidenceAlgebra.instAddGroup {𝕜 : Type u_2} {α : Type u_5} [AddGroup 𝕜] [LE α] : AddGroup (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instAddGroup = Function.Injective.addGroup (fun (f : IncidenceAlgebra 𝕜 α) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance IncidenceAlgebra.instAddCommGroup {𝕜 : Type u_2} {α : Type u_5} [AddCommGroup 𝕜] [LE α] : AddCommGroup (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instAddCommGroup = Function.Injective.addCommGroup (fun (f : IncidenceAlgebra 𝕜 α) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance IncidenceAlgebra.instOne {𝕜 : Type u_2} {α : Type u_5} [Preorder α] [DecidableEq α] [Zero 𝕜] [One 𝕜] : One (IncidenceAlgebra 𝕜 α)

The unit incidence algebra is the delta function, whose entries are 0 except on the diagonal where they are 1.

Equations

• IncidenceAlgebra.instOne = { one := { toFun := fun (a b : α) => if a = b then 1 else 0, eq_zero_of_not_le' := ⋯ } }

@[simp]

theorem IncidenceAlgebra.one_apply {𝕜 : Type u_2} {α : Type u_5} [Preorder α] [DecidableEq α] [Zero 𝕜] [One 𝕜] (a b : α) : 1 a b = if a = b then 1 else 0

instance IncidenceAlgebra.instMul {𝕜 : Type u_2} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [AddCommMonoid 𝕜] [Mul 𝕜] : Mul (IncidenceAlgebra 𝕜 α)

The multiplication operation in incidence algebras is defined on an interval by summing over all divisions into two subintervals the product of the values of the original pair of functions.

Equations

• IncidenceAlgebra.instMul = { mul := fun (f g : IncidenceAlgebra 𝕜 α) => { toFun := fun (a b : α) => ∑ x ∈ Finset.Icc a b, f a x * g x b, eq_zero_of_not_le' := ⋯ } }

@[simp]

theorem IncidenceAlgebra.mul_apply {𝕜 : Type u_2} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [AddCommMonoid 𝕜] [Mul 𝕜] (f g : IncidenceAlgebra 𝕜 α) (a b : α) : (f * g) a b = ∑ x ∈ Finset.Icc a b, f a x * g x b

instance IncidenceAlgebra.instNonUnitalNonAssocSemiring {𝕜 : Type u_2} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [NonUnitalNonAssocSemiring 𝕜] : NonUnitalNonAssocSemiring (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instNonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance IncidenceAlgebra.instNonAssocSemiring {𝕜 : Type u_2} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [NonAssocSemiring 𝕜] : NonAssocSemiring (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instNonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance IncidenceAlgebra.instSemiring {𝕜 : Type u_2} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Semiring 𝕜] : Semiring (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯

instance IncidenceAlgebra.instRing {𝕜 : Type u_2} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Ring 𝕜] : Ring (IncidenceAlgebra 𝕜 α)

Equations

• IncidenceAlgebra.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

Scalar multiplication between incidence algebras

instance IncidenceAlgebra.instSMul {𝕜 : Type u_2} {𝕝 : Type u_3} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [AddCommMonoid 𝕜] [AddCommMonoid 𝕝] [SMul 𝕜 𝕝] : SMul (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IncidenceAlgebra.smul_apply {𝕜 : Type u_2} {𝕝 : Type u_3} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [AddCommMonoid 𝕜] [AddCommMonoid 𝕝] [SMul 𝕜 𝕝] (f : IncidenceAlgebra 𝕜 α) (g : IncidenceAlgebra 𝕝 α) (a b : α) : (f • g) a b = ∑ x ∈ Finset.Icc a b, f a x • g x b

instance IncidenceAlgebra.instIsScalarTower {𝕜 : Type u_2} {𝕝 : Type u_3} {𝕞 : Type u_4} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [AddCommMonoid 𝕜] [Monoid 𝕜] [Semiring 𝕝] [AddCommMonoid 𝕞] [SMul 𝕜 𝕝] [Module 𝕝 𝕞] [DistribMulAction 𝕜 𝕞] [IsScalarTower 𝕜 𝕝 𝕞] : IsScalarTower (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α) (IncidenceAlgebra 𝕞 α)

Equations

• ⋯ = ⋯

instance IncidenceAlgebra.instModule {𝕜 : Type u_2} {𝕝 : Type u_3} {α : Type u_5} [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Semiring 𝕜] [Semiring 𝕝] [Module 𝕜 𝕝] : Module (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α)

Equations

• IncidenceAlgebra.instModule = Module.mk ⋯ ⋯

instance IncidenceAlgebra.smulWithZeroRight {𝕜 : Type u_2} {𝕝 : Type u_3} {α : Type u_5} [Zero 𝕜] [Zero 𝕝] [SMulWithZero 𝕜 𝕝] [LE α] : SMulWithZero 𝕜 (IncidenceAlgebra 𝕝 α)

Equations

• IncidenceAlgebra.smulWithZeroRight = Function.Injective.smulWithZero { toFun := DFunLike.coe, map_zero' := ⋯ } ⋯ ⋯

instance IncidenceAlgebra.moduleRight {𝕜 : Type u_2} {𝕝 : Type u_3} {α : Type u_5} [Preorder α] [Semiring 𝕜] [AddCommMonoid 𝕝] [Module 𝕜 𝕝] : Module 𝕜 (IncidenceAlgebra 𝕝 α)

Equations

• IncidenceAlgebra.moduleRight = Function.Injective.module 𝕜 { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance IncidenceAlgebra.algebraRight {𝕜 : Type u_2} {𝕝 : Type u_3} {α : Type u_5} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] [CommSemiring 𝕜] [CommSemiring 𝕝] [Algebra 𝕜 𝕝] : Algebra 𝕜 (IncidenceAlgebra 𝕝 α)

Equations

• IncidenceAlgebra.algebraRight = Algebra.mk { toFun := fun (c : 𝕜) => (algebraMap 𝕜 𝕝) c • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

The Lambda function

def IncidenceAlgebra.lambda (𝕜 : Type u_2) {α : Type u_5} [Zero 𝕜] [One 𝕜] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ⩿ x2] : IncidenceAlgebra 𝕜 α

The lambda function of the incidence algebra is the function that assigns 1 to every nonempty interval of cardinality one or two.

Equations

• IncidenceAlgebra.lambda 𝕜 = { toFun := fun (a b : α) => if a ⩿ b then 1 else 0, eq_zero_of_not_le' := ⋯ }

@[simp]

theorem IncidenceAlgebra.lambda_apply (𝕜 : Type u_2) {α : Type u_5} [Zero 𝕜] [One 𝕜] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ⩿ x2] (a b : α) : (IncidenceAlgebra.lambda 𝕜) a b = if a ⩿ b then 1 else 0

The Zeta and Möbius functions

def IncidenceAlgebra.zeta (𝕜 : Type u_2) {α : Type u_5} [Zero 𝕜] [One 𝕜] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : IncidenceAlgebra 𝕜 α

The zeta function of the incidence algebra is the function that assigns 1 to every nonempty interval, convolution with this function sums functions over intervals.

Equations

• IncidenceAlgebra.zeta 𝕜 = { toFun := fun (a b : α) => if a ≤ b then 1 else 0, eq_zero_of_not_le' := ⋯ }

@[simp]

theorem IncidenceAlgebra.zeta_apply {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [One 𝕜] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (a b : α) : (IncidenceAlgebra.zeta 𝕜) a b = if a ≤ b then 1 else 0

theorem IncidenceAlgebra.zeta_of_le {𝕜 : Type u_2} {α : Type u_5} [Zero 𝕜] [One 𝕜] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {a b : α} (h : a ≤ b) : (IncidenceAlgebra.zeta 𝕜) a b = 1

theorem IncidenceAlgebra.zeta_mul_zeta {𝕜 : Type u_2} {α : Type u_5} [Semiring 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (a b : α) : (IncidenceAlgebra.zeta 𝕜 * IncidenceAlgebra.zeta 𝕜) a b = ↑(Finset.Icc a b).card

theorem IncidenceAlgebra.zeta_mul_kappa {𝕜 : Type u_2} {α : Type u_5} [Semiring 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (a b : α) : (IncidenceAlgebra.zeta 𝕜 * IncidenceAlgebra.zeta 𝕜) a b = ↑(Finset.Icc a b).card

def IncidenceAlgebra.mu (𝕜 : Type u_2) {α : Type u_5} [AddCommGroup 𝕜] [One 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] : IncidenceAlgebra 𝕜 α

The Möbius function which inverts zeta as an element of the incidence algebra.

Equations

• IncidenceAlgebra.mu 𝕜 = { toFun := IncidenceAlgebra.muFun 𝕜, eq_zero_of_not_le' := ⋯ }

theorem IncidenceAlgebra.mu_apply {𝕜 : Type u_2} {α : Type u_5} [AddCommGroup 𝕜] [One 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : (IncidenceAlgebra.mu 𝕜) a b = if a = b then 1 else -∑ x ∈ Finset.Ico a b, (IncidenceAlgebra.mu 𝕜) a x

@[simp]

theorem IncidenceAlgebra.mu_self {𝕜 : Type u_2} {α : Type u_5} [AddCommGroup 𝕜] [One 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] (a : α) : (IncidenceAlgebra.mu 𝕜) a a = 1

theorem IncidenceAlgebra.mu_eq_neg_sum_Ico_of_ne {𝕜 : Type u_2} {α : Type u_5} [AddCommGroup 𝕜] [One 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] {a b : α} (hab : a ≠ b) : (IncidenceAlgebra.mu 𝕜) a b = -∑ x ∈ Finset.Ico a b, (IncidenceAlgebra.mu 𝕜) a x

theorem IncidenceAlgebra.sum_Icc_mu_right {𝕜 : Type u_2} {α : Type u_5} [AddCommGroup 𝕜] [One 𝕜] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : ∑ x ∈ Finset.Icc a b, (IncidenceAlgebra.mu 𝕜) a x = if a = b then 1 else 0

theorem IncidenceAlgebra.mu_mul_zeta (𝕜 : Type u_2) (α : Type u_5) [AddCommGroup 𝕜] [MulOneClass 𝕜] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : IncidenceAlgebra.mu 𝕜 * IncidenceAlgebra.zeta 𝕜 = 1

theorem IncidenceAlgebra.mu_eq_neg_sum_Ioc_of_ne {𝕜 : Type u_2} {α : Type u_5} [Ring 𝕜] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] {a b : α} (hab : a ≠ b) : (IncidenceAlgebra.mu 𝕜) a b = -∑ x ∈ Finset.Ioc a b, (IncidenceAlgebra.mu 𝕜) x b

theorem IncidenceAlgebra.zeta_mul_mu {𝕜 : Type u_2} {α : Type u_5} [Ring 𝕜] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : IncidenceAlgebra.zeta 𝕜 * IncidenceAlgebra.mu 𝕜 = 1

theorem IncidenceAlgebra.sum_Icc_mu_left {𝕜 : Type u_2} {α : Type u_5} [Ring 𝕜] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : ∑ x ∈ Finset.Icc a b, (IncidenceAlgebra.mu 𝕜) x b = if a = b then 1 else 0

@[simp]

theorem IncidenceAlgebra.mu_toDual (𝕜 : Type u_2) {α : Type u_5} [Ring 𝕜] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : (IncidenceAlgebra.mu 𝕜) (OrderDual.toDual a) (OrderDual.toDual b) = (IncidenceAlgebra.mu 𝕜) b a

@[simp]

theorem IncidenceAlgebra.mu_ofDual (𝕜 : Type u_2) {α : Type u_5} [Ring 𝕜] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : αᵒᵈ) : (IncidenceAlgebra.mu 𝕜) (OrderDual.ofDual a) (OrderDual.ofDual b) = (IncidenceAlgebra.mu 𝕜) b a

theorem IncidenceAlgebra.moebius_inversion_top {𝕜 : Type u_2} {α : Type u_5} [Ring 𝕜] [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] [DecidableEq α] (f g : α → 𝕜) (h : ∀ (x : α), g x = ∑ y ∈ Finset.Ici x, f y) (x : α) : f x = ∑ y ∈ Finset.Ici x, (IncidenceAlgebra.mu 𝕜) x y * g y

A general form of Möbius inversion. Based on lemma 2.1.2 of Incidence Algebras by Spiegel and O'Donnell.

theorem IncidenceAlgebra.moebius_inversion_bot {𝕜 : Type u_2} {α : Type u_5} [Ring 𝕜] [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] [DecidableEq α] (f g : α → 𝕜) (h : ∀ (x : α), g x = ∑ y ∈ Finset.Iic x, f y) (x : α) : f x = ∑ y ∈ Finset.Iic x, (IncidenceAlgebra.mu 𝕜) y x * g y

A general form of Möbius inversion. Based on lemma 2.1.3 of Incidence Algebras by Spiegel and O'Donnell.

theorem IncidenceAlgebra.zeta_prod_apply (𝕜 : Type u_2) {α : Type u_5} {β : Type u_6} [Ring 𝕜] [Preorder α] [Preorder β] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (a b : α × β) : (IncidenceAlgebra.zeta 𝕜) a b = (IncidenceAlgebra.zeta 𝕜) a.1 b.1 * (IncidenceAlgebra.zeta 𝕜) a.2 b.2

theorem IncidenceAlgebra.zeta_prod_mk (𝕜 : Type u_2) {α : Type u_5} {β : Type u_6} [Ring 𝕜] [Preorder α] [Preorder β] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (a₁ a₂ : α) (b₁ b₂ : β) : (IncidenceAlgebra.zeta 𝕜) (a₁, b₁) (a₂, b₂) = (IncidenceAlgebra.zeta 𝕜) a₁ a₂ * (IncidenceAlgebra.zeta 𝕜) b₁ b₂

def IncidenceAlgebra.prod {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [Ring 𝕜] [Preorder α] [Preorder β] (f : IncidenceAlgebra 𝕜 α) (g : IncidenceAlgebra 𝕜 β) : IncidenceAlgebra 𝕜 (α × β)

The cartesian product of two incidence algebras.

Equations

• f.prod g = { toFun := fun (x y : α × β) => f x.1 y.1 * g x.2 y.2, eq_zero_of_not_le' := ⋯ }

theorem IncidenceAlgebra.prod_mk {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [Ring 𝕜] [Preorder α] [Preorder β] (f : IncidenceAlgebra 𝕜 α) (g : IncidenceAlgebra 𝕜 β) (a₁ a₂ : α) (b₁ b₂ : β) : (f.prod g) (a₁, b₁) (a₂, b₂) = f a₁ a₂ * g b₁ b₂

@[simp]

theorem IncidenceAlgebra.prod_apply {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [Ring 𝕜] [Preorder α] [Preorder β] (f : IncidenceAlgebra 𝕜 α) (g : IncidenceAlgebra 𝕜 β) (x y : α × β) : (f.prod g) x y = f x.1 y.1 * g x.2 y.2

theorem IncidenceAlgebra.prod_mul_prod' {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [Ring 𝕜] [Preorder α] [Preorder β] (f₁ f₂ : IncidenceAlgebra 𝕜 α) (g₁ g₂ : IncidenceAlgebra 𝕜 β) [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] (h : ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β), f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)) : f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)

This is a version of IncidenceAlgebra.prod_mul_prod that works over non-commutative rings.

@[simp]

theorem IncidenceAlgebra.one_prod_one {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [Ring 𝕜] [Preorder α] [Preorder β] [DecidableEq α] [DecidableEq β] : IncidenceAlgebra.prod 1 1 = 1

@[simp]

theorem IncidenceAlgebra.zeta_prod_zeta {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [Ring 𝕜] [Preorder α] [Preorder β] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] : (IncidenceAlgebra.zeta 𝕜).prod (IncidenceAlgebra.zeta 𝕜) = IncidenceAlgebra.zeta 𝕜

@[simp]

theorem IncidenceAlgebra.prod_mul_prod {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [CommRing 𝕜] [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] (f₁ f₂ : IncidenceAlgebra 𝕜 α) (g₁ g₂ : IncidenceAlgebra 𝕜 β) : f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)

@[simp]

theorem IncidenceAlgebra.mu_prod_mu (𝕜 : Type u_2) {α : Type u_5} {β : Type u_6} [Ring 𝕜] [PartialOrder α] [PartialOrder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableEq α] [DecidableEq β] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] : (IncidenceAlgebra.mu 𝕜).prod (IncidenceAlgebra.mu 𝕜) = IncidenceAlgebra.mu 𝕜

The Möbius function on a product order. Based on lemma 2.1.13 of Incidence Algebras by Spiegel and O'Donnell.