Incidence algebras

Content created by Egbert Rijke and Garrett Figueroa.

Created on 2024-11-14.
Last modified on 2024-11-14.

module order-theory.incidence-algebras where
Imports 
open import commutative-algebra.commutative-rings

open import foundation.dependent-pair-types
open import foundation.inhabited-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types

open import order-theory.interval-subposets
open import order-theory.locally-finite-posets
open import order-theory.posets

Idea

For a locally finite poset ‘P’ and commutative ring ‘R’, there is a canonical ‘R’-associative algebra whose underlying ‘R’-module are the set-maps from the nonempty intervals of ‘P’ to ‘R’ (which we constructify as the inhabited intervals), and whose multiplication is given by a “convolution” of maps. This is the incidence algebra of ‘P’ over ‘R’.

Definition

module _
  {l1 l2 l3 : Level} (P : Poset l1 l2) (loc-fin : is-locally-finite-Poset P)
  (x y : type-Poset P) (R : Commutative-Ring l3)
  where

  interval-map : UU (l1 ⊔ l2 ⊔ l3)
  interval-map = inhabited-interval P → type-Commutative-Ring R

WIP: complete this definition after R-modules have been defined. Defining convolution of maps would be aided as well with a lemma on ‘unordered’ addition in abelian groups over finite sets.

Recent changes