Lemma 4.9: weights on representation-finite posets #
lem:poset-weights (scalar-normalization.tex): "If the incidence
algebra of a finite poset R is representation-finite, every additive weight,
with values in any abelian group, has the form w(x,y) = ζ_y − ζ_x."
Proof of the source: "Remove a minimal element s and put U = {y : s < y}.
Distinct connected components of U lie in distinct components of R ∖ {s}.
Otherwise, put a one-dimensional space at every vertex, assign the map one to
every comparison outside s, and assign maps λ ∈ k* from s to one
component of U and one to the others. These are representations. An
isomorphism must have the same scalar at all vertices of each component of
R ∖ {s}. Two components of U in the same such component therefore force
equality of the parameters. This produces infinitely many isomorphism classes
of fixed dimension, contrary to finite representation type. […] By induction
normalize all weights on R ∖ {s} to zero. The remaining weights from s are
constant on each component of U. Adjust the object values separately on the
corresponding components of R ∖ {s} to remove these constants."
The representations are right modules over the incidence algebra on a convex
connected set D (thinRep); the source restricts them to the component of
s, where they are indecomposable. The removal of minimal elements runs
through the up-sets of R, whose components are convex in R, so the
representations of all steps are representations of the incidence algebra of
R itself (no corner argument is needed).
Comparability.
Instances For
def
MultiplicativeBasisDeformations.PosetWeights.ConnIn
{P : Type v}
[PartialOrder P]
(Q : Set P)
(x y : P)
:
Connectedness inside a set, through comparable elements of the set.
Instances For
def
MultiplicativeBasisDeformations.PosetWeights.IsConvex
{P : Type v}
[PartialOrder P]
(D : Set P)
:
A convex set.
Instances For
Thin representations #
def
MultiplicativeBasisDeformations.PosetWeights.act
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
(D : Set P)
[DecidablePred fun (x : P) => x ∈ D]
(ρ : P → P → k)
(a : IncidenceAlgebra k P)
(v : ↑D → k)
:
↑D → k
The action of the incidence algebra on k^D through the scalars ρ.
Instances For
structure
MultiplicativeBasisDeformations.PosetWeights.IsMult
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
(D : Set P)
(ρ : P → P → k)
:
Multiplicativity of ρ along chains in D, with ρ x x = 1.
- refl (x : P) : x ∈ D → ρ x x = 1
- trans (x y z : P) : x ∈ D → y ∈ D → z ∈ D → x ≤ y → y ≤ z → ρ x z = ρ x y * ρ y z
Instances For
theorem
MultiplicativeBasisDeformations.PosetWeights.sum_D_eq_Icc
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
(hD : IsConvex D)
(x z : ↑D)
(f : P → k)
:
(∑ y : ↑D, if ↑x ≤ ↑y ∧ ↑y ≤ ↑z then f ↑y else 0) = ∑ y ∈ Finset.Icc ↑x ↑z, f y
theorem
MultiplicativeBasisDeformations.PosetWeights.act_mul
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
(a b : IncidenceAlgebra k P)
(v : ↑D → k)
:
def
MultiplicativeBasisDeformations.PosetWeights.Car
{k : Type u}
{P : Type v}
(D : Set P)
(_ρ : P → P → k)
:
Type (max u v)
The carrier of the thin representation.
Instances For
@[instance_reducible]
instance
MultiplicativeBasisDeformations.PosetWeights.instAddCommGroupCar
{k : Type u}
[Field k]
{P : Type v}
{D : Set P}
{ρ : P → P → k}
:
AddCommGroup (Car D ρ)
@[instance_reducible]
instance
MultiplicativeBasisDeformations.PosetWeights.instModuleCar
{k : Type u}
[Field k]
{P : Type v}
{D : Set P}
{ρ : P → P → k}
:
Module k (Car D ρ)
def
MultiplicativeBasisDeformations.PosetWeights.repModule
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
:
Module (IncidenceAlgebra k P)ᵐᵒᵖ (Car D ρ)
The right module structure.
Instances For
def
MultiplicativeBasisDeformations.PosetWeights.thinRep
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
:
RightModuleCat (IncidenceAlgebra k P)
The thin representation k^D with maps ρ.
Instances For
Homomorphisms between thin representations are diagonal #
def
MultiplicativeBasisDeformations.PosetWeights.sgl
{P : Type v}
[PartialOrder P]
[DecidableEq P]
(k : Type u)
[Field k]
(x y : P)
(h : x ≤ y)
:
IncidenceAlgebra k P
The matrix unit at x ≤ y.
Instances For
theorem
MultiplicativeBasisDeformations.PosetWeights.act_sgl
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(x y : ↑D)
(h : ↑x ≤ ↑y)
(v : ↑D → k)
:
theorem
MultiplicativeBasisDeformations.PosetWeights.act_smul_sgl
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(r : k)
(x y : ↑D)
(h : ↑x ≤ ↑y)
(v : ↑D → k)
:
def
MultiplicativeBasisDeformations.PosetWeights.dlt
{P : Type v}
[DecidableEq P]
{D : Set P}
(k : Type u)
[Field k]
(x : ↑D)
:
↑D → k
The basis vector at x.
Instances For
theorem
MultiplicativeBasisDeformations.PosetWeights.hom_diagonal
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
{ρ' : P → P → k}
(hρ' : IsMult D ρ')
(φ : thinRep hD hρ ⟶ thinRep hD hρ')
:
∃ (c : ↑D → k),
(∀ (v : ↑(thinRep hD hρ)) (x : ↑D), (ModuleCat.Hom.hom φ) v x = c x * v x) ∧ ∀ (x y : ↑D), ↑x ≤ ↑y → c x * ρ' ↑x ↑y = c y * ρ ↑x ↑y
Homomorphisms of thin representations are diagonal, with
c_x ρ'(x,y) = c_y ρ(x,y).
Finiteness and indecomposability #
theorem
MultiplicativeBasisDeformations.PosetWeights.act_algebraMap
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hρ : IsMult D ρ)
(c : k)
(v : ↑D → k)
:
act D ρ ((algebraMap k (IncidenceAlgebra k P)) c) v = c • v
def
MultiplicativeBasisDeformations.PosetWeights.toPi
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
:
↑(thinRep hD hρ) →ₗ[k] ↑D → k
The identification with k^D is k-linear.
Instances For
theorem
MultiplicativeBasisDeformations.PosetWeights.thinRep_finite
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
:
Module.Finite k ↑(thinRep hD hρ)
theorem
MultiplicativeBasisDeformations.PosetWeights.connIn_mem_iff
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{Q : Set P}
{a b : P}
(h : ConnIn Q a b)
:
a ∈ Q ↔ b ∈ Q
A connected set.
Instances For
theorem
MultiplicativeBasisDeformations.PosetWeights.const_of_connIn
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{α : Type u_1}
{Q : Set P}
(c : P → α)
(hc : ∀ (x y : P), x ∈ Q → y ∈ Q → x ≤ y → c x = c y)
{a b : P}
(h : ConnIn Q a b)
:
c a = c b
theorem
MultiplicativeBasisDeformations.PosetWeights.end_scalar
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
(hρ0 : ∀ (x y : ↑D), ↑x ≤ ↑y → ρ ↑x ↑y ≠ 0)
(hconn : IsConn D)
(x₀ : ↑D)
(φ : thinRep hD hρ ⟶ thinRep hD hρ)
:
∃ (c : k), ∀ (v : ↑(thinRep hD hρ)) (x : ↑D), (ModuleCat.Hom.hom φ) v x = c * v x
Endomorphisms of a connected thin representation are scalars.
theorem
MultiplicativeBasisDeformations.PosetWeights.end_isLocalRing
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
(hρ0 : ∀ (x y : ↑D), ↑x ≤ ↑y → ρ ↑x ↑y ≠ 0)
(hconn : IsConn D)
(x₀ : ↑D)
:
IsLocalRing (CategoryTheory.End (thinRep hD hρ))
theorem
MultiplicativeBasisDeformations.PosetWeights.thinRep_indecomposable
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
(hρ0 : ∀ (x y : ↑D), ↑x ≤ ↑y → ρ ↑x ↑y ≠ 0)
(hconn : IsConn D)
(x₀ : ↑D)
:
CategoryTheory.Indecomposable (thinRep hD hρ)
theorem
MultiplicativeBasisDeformations.PosetWeights.thinRep_isFiniteIndecomposable
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
(hρ0 : ∀ (x y : ↑D), ↑x ≤ ↑y → ρ ↑x ↑y ≠ 0)
(hconn : IsConn D)
(x₀ : ↑D)
:
IsFiniteIndecomposable k (IncidenceAlgebra k P) (thinRep hD hρ)
theorem
MultiplicativeBasisDeformations.PosetWeights.iso_diagonal
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{D : Set P}
[DecidablePred fun (x : P) => x ∈ D]
{ρ : P → P → k}
(hD : IsConvex D)
(hρ : IsMult D ρ)
{ρ' : P → P → k}
(hρ' : IsMult D ρ')
(e : thinRep hD hρ ≅ thinRep hD hρ')
:
∃ (c : ↑D → k), (∀ (x : ↑D), c x ≠ 0) ∧ ∀ (x y : ↑D), ↑x ≤ ↑y → c x * ρ' ↑x ↑y = c y * ρ ↑x ↑y
Isomorphic thin representations differ by object values.
Separation of the components of U #
theorem
MultiplicativeBasisDeformations.PosetWeights.connIn_mono
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{Q Q' : Set P}
(h : Q ⊆ Q')
{a b : P}
(hab : ConnIn Q a b)
:
ConnIn Q' a b
theorem
MultiplicativeBasisDeformations.PosetWeights.connIn_restrict
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
{Q D : Set P}
(hDQ : D ⊆ Q)
(hcl : ∀ (a b : P), a ∈ D → b ∈ Q → Comp a b → b ∈ D)
{a b : P}
(hab : ConnIn Q a b)
:
a ∈ D → ConnIn D a b ∧ b ∈ D
A path inside Q from a point of a subset D closed under comparability
in Q stays in D.
theorem
MultiplicativeBasisDeformations.PosetWeights.sep
{k : Type u}
[Field k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
[Infinite k]
(hrep : IsRepresentationFinite k (IncidenceAlgebra k P))
(Q : Set P)
(hQ : IsUpperSet Q)
(s : P)
(hs : s ∈ Q)
(hmin : ∀ x ∈ Q, ¬x < s)
(y₁ y₂ : P)
(h₁ : s < y₁)
(h₂ : s < y₂)
(hc : ConnIn (Q \ {s}) y₁ y₂)
:
ConnIn {y : P | s < y} y₁ y₂
Distinct components of U lie in distinct components of Q ∖ {s}
(scalar-normalization.tex), for an up-set Q and a minimal s ∈ Q.
Normalizing weights #
theorem
MultiplicativeBasisDeformations.PosetWeights.weights_upset
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
(hsep :
∀ (Q : Set P),
IsUpperSet Q →
∀ s ∈ Q,
(∀ x ∈ Q, ¬x < s) → ∀ (y₁ y₂ : P), s < y₁ → s < y₂ → ConnIn (Q \ {s}) y₁ y₂ → ConnIn {y : P | s < y} y₁ y₂)
{G : Type u_1}
[AddCommGroup G]
(wt : P → P → G)
(hwt : ∀ (x y z : P), x ≤ y → y ≤ z → wt x z = wt x y + wt y z)
(n : ℕ)
(Q : Finset P)
:
Q.card = n → IsUpperSet ↑Q → ∃ (ζ : P → G), ∀ (x y : P), x ∈ Q → y ∈ Q → x ≤ y → wt x y = ζ y - ζ x
The induction of the source, over the up-sets of R.
theorem
MultiplicativeBasisDeformations.posetWeights_of
{k : Type u}
[Field k]
[Infinite k]
{P : Type v}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
(hP : IsRepresentationFinite k (IncidenceAlgebra k P))
{G : Type u_1}
[AddCommGroup G]
(wt : P → P → G)
(hwt : ∀ (x y z : P), x ≤ y → y ≤ z → wt x z = wt x y + wt y z)
:
∃ (ζ : P → G), ∀ (x y : P), x ≤ y → wt x y = ζ y - ζ x
Lemma 4.9 (lem:poset-weights), over an infinite field.
theorem
MultiplicativeBasisDeformations.ratio_of_mult
{k : Type u_1}
[Field k]
[Infinite k]
{P : Type u_2}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
[DecidableLE P]
(hP : IsRepresentationFinite k (IncidenceAlgebra k P) ∨ IsRepresentationFinite k (IncidenceAlgebra k Pᵒᵈ))
(μ : P → P → k)
(hμ0 : ∀ (a b : P), a ≤ b → μ a b ≠ 0)
(hμmul : ∀ (a b c : P), a ≤ b → b ≤ c → μ a c = μ a b * μ b c)
:
∃ (Z : P → k), (∀ (a : P), Z a ≠ 0) ∧ ∀ (a b : P), a ≤ b → μ a b = Z a / Z b
Lemma 4.9 for multiplicative k*-weights, with either orientation of the
incidence algebra: μ(a,b) = Z_a / Z_b.