def PlanarRook.Algebra {k : Type} (n : ℕ) (δ : k) : Type

The planar rook algebra over a field k with parameter δ consists of elements which are formal k-linear combinations of planar rook diagrams on n strands.

The multiplication is more complicated and is given by monoid multiplication of diagrams, with a factor of δ raised to the number of dangling strands after multiplication.

Equations

• PlanarRook.Algebra n δ = (PlanarRook.Diagram n n → k)

def PlanarRook.Algebra.ext {k : Type} {n : ℕ} {δ : k} {x y : Algebra n δ} : (∀ (d : Diagram n n), x d = y d) → x = y

Equations

• ⋯ = ⋯

theorem PlanarRook.Algebra.ext_iff {k : Type} {n : ℕ} {δ : k} {x y : Algebra n δ} : x = y ↔ ∀ (d : Diagram n n), x d = y d

instance PlanarRook.Algebra.instAddCommMonoid {k : Type} [Field k] (δ : k) {n : ℕ} : AddCommMonoid (Algebra n δ)

Equations

• PlanarRook.Algebra.instAddCommMonoid δ = inferInstanceAs (AddCommMonoid (PlanarRook.Diagram n n → k))

instance PlanarRook.Algebra.instAddCommGroup {k : Type} [Field k] (δ : k) {n : ℕ} : AddCommGroup (Algebra n δ)

Equations

• PlanarRook.Algebra.instAddCommGroup δ = inferInstanceAs (AddCommGroup (PlanarRook.Diagram n n → k))

@[simp]

theorem PlanarRook.Algebra.zero_coeff {k : Type} [Field k] (δ : k) {n : ℕ} (d : Diagram n n) : 0 d = 0

@[simp]

theorem PlanarRook.Algebra.add_coeff {k : Type} [Field k] (δ : k) {n : ℕ} (x₁ x₂ : Algebra n δ) (d : Diagram n n) : (x₁ + x₂) d = x₁ d + x₂ d

instance PlanarRook.Algebra.instModule {k : Type} [Field k] (δ : k) {n : ℕ} : Module k (Algebra n δ)

The planar rook algebra is a vector space over k.

Equations

• PlanarRook.Algebra.instModule δ = Pi.module (PlanarRook.Diagram n n) (fun (a : PlanarRook.Diagram n n) => k) k

def PlanarRook.Algebra.diagram_basis {k : Type} [Field k] (δ : k) {n : ℕ} [DecidableEq k] : Module.Basis (Diagram n n) k (Algebra n δ)

The obvious k basis of the PlanarRookAlgebra is the diagram basis.

In fact, this is how it is naturally defined, as the maps from diagrams to the underlying ring. However, the "basis" also requires some assurances about finiteness that we provide explicitly in this instance.

Note: This could probably be made more general for arbitrary fintypes.

Equations

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

def PlanarRook.Algebra.single {k : Type} [Field k] (δ : k) {n : ℕ} : Diagram n n → k → Algebra n δ

Equations

• PlanarRook.Algebra.single δ = Pi.single

@[simp]

def PlanarRook.Algebra.single_apply {k : Type} [Field k] (δ : k) {n : ℕ} (d₁ d₂ : Diagram n n) (c : k) : single δ d₁ c d₂ = if d₂ = d₁ then c else 0

Equations

• ⋯ = ⋯

@[simp]

theorem PlanarRook.Algebra.smul_single {k : Type} [Field k] (δ : k) {n : ℕ} (d₁ : Diagram n n) (c₁ c₂ : k) : c₁ • single δ d₁ c₂ = single δ d₁ (c₁ * c₂)

@[simp]

theorem PlanarRook.Algebra.smul_single' {k : Type} [Field k] (δ : k) {n : ℕ} (d₁ : Diagram n n) (c : k) : c • single δ d₁ 1 = single δ d₁ c

theorem PlanarRook.Algebra.sum_single {k : Type} [Field k] (δ : k) {n : ℕ} (x : Algebra n δ) : x = ∑ d : Diagram n n, single δ d (x d)

theorem PlanarRook.Algebra.add_single {k : Type} [Field k] (δ : k) {n : ℕ} (d : Diagram n n) (c₁ c₂ : k) : single δ d (c₁ + c₂) = single δ d c₁ + single δ d c₂

def PlanarRook.Algebra.mul {k : Type} [Field k] (δ : k) {n : ℕ} (x y : Algebra n δ) : Algebra n δ

Multiplication in the planar rook algebra depends on a paramter δ

This paramter is raised to the exponent of the number of dangling strands after monoid multiplication.

Equations

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

def PlanarRook.Algebra.one {k : Type} [Field k] (δ : k) {n : ℕ} : Algebra n δ

Equations

• PlanarRook.Algebra.one δ = PlanarRook.Algebra.single δ (PlanarRook.Diagram.id n) 1

def PlanarRook.Algebra.one_apply {k : Type} [Field k] (δ : k) {n : ℕ} (d : Diagram n n) : one δ d = if Diagram.id n = d then 1 else 0

Equations

• ⋯ = ⋯

instance PlanarRook.Algebra.instMul {k : Type} [Field k] (δ : k) {n : ℕ} : Mul (Algebra n δ)

Equations

• PlanarRook.Algebra.instMul δ = { mul := PlanarRook.Algebra.mul δ }

theorem PlanarRook.Algebra.mul_def {k : Type} [Field k] (δ : k) {n : ℕ} (x y : Algebra n δ) : x * y = ∑ d₁ : Diagram n n, ∑ d₂ : Diagram n n, (x d₁ * y d₂) • single δ (d₁ * d₂) (δ ^ Monoid.mul_exponent d₁ d₂)

theorem PlanarRook.Algebra.mul_apply {k : Type} [Field k] (δ : k) {n : ℕ} {m : Diagram n n} (x y : Algebra n δ) : (x * y) m = ∑ d₁ : Diagram n n, ∑ d₂ : Diagram n n, if d₁ * d₂ = m then x d₁ * y d₂ * δ ^ Monoid.mul_exponent d₁ d₂ else 0

instance PlanarRook.Algebra.nonUnitalNonAssocSemiring {k : Type} [Field k] (δ : k) {n : ℕ} : NonUnitalNonAssocSemiring (Algebra n δ)

Equations

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

theorem PlanarRook.Algebra.mul_single {k : Type} [Field k] (δ : k) {n : ℕ} (x : Algebra n δ) (d₁ : Diagram n n) (c : k) : x * single δ d₁ c = ∑ d₂ : Diagram n n, x d₂ • single δ (d₂ * d₁) (c * δ ^ Monoid.mul_exponent d₂ d₁)

theorem PlanarRook.Algebra.single_mul {k : Type} [Field k] (δ : k) {n : ℕ} (x : Algebra n δ) (d₁ : Diagram n n) (c : k) : single δ d₁ c * x = ∑ d₂ : Diagram n n, x d₂ • single δ (d₁ * d₂) (c * δ ^ Monoid.mul_exponent d₁ d₂)

theorem PlanarRook.Algebra.mul_single_single {k : Type} [Field k] (δ : k) {n : ℕ} (d₁ d₂ : Diagram n n) (c₁ c₂ : k) : single δ d₁ c₁ * single δ d₂ c₂ = single δ (d₁ * d₂) (c₁ * c₂ * δ ^ Monoid.mul_exponent d₁ d₂)

Associativity of multiplication

We can now show that multiplication is associative. That is, we have a non-unital semiring structure on the planar rook algebra. We will later show that it is unital, and hence a ring.

instance PlanarRook.Algebra.nonUnitalSemiring {k : Type} [Field k] (δ : k) {n : ℕ} : NonUnitalSemiring (Algebra n δ)

Equations

• PlanarRook.Algebra.nonUnitalSemiring δ = { toNonUnitalNonAssocSemiring := PlanarRook.Algebra.nonUnitalNonAssocSemiring δ, mul_assoc := ⋯ }

instance PlanarRook.Algebra.hasOne {k : Type} [Field k] (δ : k) {n : ℕ} : One (Algebra n δ)

Equations

• PlanarRook.Algebra.hasOne δ = { one := PlanarRook.Algebra.one δ }

theorem PlanarRook.Algebra.one_def {k : Type} [Field k] (δ : k) {n : ℕ} : 1 = one δ

def PlanarRook.Algebra.one_is {k : Type} [Field k] (δ : k) {n : ℕ} : 1 = single δ (Diagram.id n) 1

Equations

• ⋯ = ⋯

instance PlanarRook.Algebra.addGroupWithOne {k : Type} [Field k] (δ : k) {n : ℕ} : AddGroupWithOne (Algebra n δ)

Equations

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

instance PlanarRook.Algebra.is_semiring {k : Type} [Field k] (δ : k) {n : ℕ} : Semiring (Algebra n δ)

Equations

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

def PlanarRook.Algebra.single_one_ring_hom {k : Type} [Field k] (δ : k) {n : ℕ} : k →+* Algebra n δ

Equations

• PlanarRook.Algebra.single_one_ring_hom δ = { toFun := fun (c : k) => c • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

instance PlanarRook.Algebra.is_algebra {k : Type} [Field k] {n : ℕ} (δ : k) : _root_.Algebra k (Algebra n δ)

Equations

• PlanarRook.Algebra.is_algebra δ = { toSMul := DistribMulAction.toDistribSMul.toSMul, algebraMap := PlanarRook.Algebra.single_one_ring_hom δ, commutes' := ⋯, smul_def' := ⋯ }

theorem PlanarRook.Algebra.algebra_map {k : Type} [Field k] (δ : k) {n : ℕ} : algebraMap k (Algebra n δ) = single_one_ring_hom δ

def PlanarRook.Algebra.parameter_independence {k : Type} [Field k] (n : ℕ) (δ₁ : k) (δ₁_nonzero : δ₁ ≠ 0) : Algebra n δ₁ ≃ₐ[k] Algebra n 1

The planar rook algebra is independent of the parameter δ, up to algebra isomorphism, as long as it is not zero.

This is to say, there are only "two" planar rook algebras, the one where δ = 0 and the one where δ is nonzero (and might as well be 1).

Equations

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

instance PlanarRook.Algebra.ringConGen {k : Type} [Field k] (δ : k) {n : ℕ} : Ring (Algebra n δ)

Equations

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

theorem PlanarRook.Algebra.diagram_basis_mul {k : Type} [Field k] (δ : k) [DecidableEq k] {n : ℕ} (a b : Diagram n n) : (diagram_basis δ) a * (diagram_basis δ) b = δ ^ Monoid.mul_exponent a b • (diagram_basis δ) (a * b)

def PlanarRook.Algebra.diagram_basis' {k : Type} [Field k] (δ : k) [DecidableEq k] {n : ℕ} : Module.Basis ((μ : Fin (n + 1)) × { S : Finset (Fin n) // S.card = ↑μ } × { S : Finset (Fin n) // S.card = ↑μ }) k (Algebra n δ)

Equations

• PlanarRook.Algebra.diagram_basis' δ = (PlanarRook.Algebra.diagram_basis δ).reindex PlanarRook.Diagram.pi_iso₂

theorem PlanarRook.Algebra.diagram_basis'_mul {k : Type} [Field k] (δ : k) [DecidableEq k] {n : ℕ} (a b : (μ : Fin (n + 1)) × { S : Finset (Fin n) // S.card = ↑μ } × { S : Finset (Fin n) // S.card = ↑μ }) : (diagram_basis' δ) a * (diagram_basis' δ) b = δ ^ Monoid.mul_exponent (Diagram.pi_iso₂.invFun a) (Diagram.pi_iso₂.invFun b) • (diagram_basis' δ) (Diagram.pi_iso₂.toFun (Diagram.pi_iso₂.invFun a * Diagram.pi_iso₂.invFun b))

The algebra anti-involution

noncomputable def PlanarRook.Algebra.ι {k : Type} [Field k] [DecidableEq k] {n : ℕ} {δ : k} : Algebra n δ →ₗ[k] Algebra n δ

Equations

• PlanarRook.Algebra.ι = ((PlanarRook.Algebra.diagram_basis δ).constr k) (⇑(PlanarRook.Algebra.diagram_basis δ) ∘ PlanarRook.Diagram.ι)

def PlanarRook.Algebra.diagram_basis_swap {n : ℕ} : (μ : Fin (n + 1)) × { S : Finset (Fin n) // S.card = ↑μ } × { S : Finset (Fin n) // S.card = ↑μ } → (μ : Fin (n + 1)) × { S : Finset (Fin n) // S.card = ↑μ } × { S : Finset (Fin n) // S.card = ↑μ }

Equations

• PlanarRook.Algebra.diagram_basis_swap ⟨i, (S, T)⟩ = ⟨i, (T, S)⟩

theorem PlanarRook.Algebra.diagram_basis'_ι {k : Type} [Field k] (δ : k) [DecidableEq k] {n : ℕ} : ι = ((diagram_basis' δ).constr k) (⇑(diagram_basis' δ) ∘ diagram_basis_swap)

def PlanarRook.Algebra.foobar {k : Type} [Field k] (δ : k) [DecidableEq k] {n : ℕ} : (fun (x : (μ : Fin (n + 1)) × { S : Finset (Fin n) // S.card = ↑μ } × { S : Finset (Fin n) // S.card = ↑μ }) => match x with | ⟨μ, (s, t)⟩ => (diagram_basis' δ) ⟨μ, (t, s)⟩) = ⇑(diagram_basis' δ) ∘ diagram_basis_swap

Equations

• ⋯ = ⋯

theorem PlanarRook.Algebra.ι_anti {k : Type} [Field k] (δ : k) [DecidableEq k] {n : ℕ} (a b : Algebra n δ) : ι (a * b) = ι b * ι a