Tensor products of normal crystals

For normal crystals B₁ and B₂ over a root datum with a base, the tensor product B₁ ⊗ B₂ is the normal crystal on B₁ × B₂ with weight wt (x₁, x₂) = wt x₁ + wt x₂, string lengths

• ε i (x₁, x₂) = ε i x₁ + (ε i x₂ - φ i x₁),
• φ i (x₁, x₂) = φ i x₂ + (φ i x₁ - ε i x₂)

(truncated subtraction in ℕ), and root operators acting on one factor:

• e i (x₁, x₂) = (e i x₁, x₂) if ε i x₂ ≤ φ i x₁, and (x₁, e i x₂) otherwise;
• f i (x₁, x₂) = (f i x₁, x₂) if ε i x₂ < φ i x₁, and (x₁, f i x₂) otherwise.

If the operator on the factor it acts on returns none (standing for 0), the operator on the tensor product returns none as well.

Tie convention. This is Kashiwara's convention: on a tie φ i x₁ = ε i x₂ the raising operator acts on the left factor and the lowering operator on the right factor. It is the convention under which Littelmann's concatenation π₁ * π₂ of paths corresponds to π₁ ⊗ π₂: on the concatenation, e i changes the path containing the first time at which the height ⟨π(t), α_i^∨⟩ attains its minimum, and f i the path containing the last such time. Bump and Schilling use the opposite convention, which is obtained from this one by exchanging the two factors.

In Kashiwara's form the string lengths are ε i (x₁, x₂) = max (ε i x₁) (ε i x₂ - ⟨wt x₁, α_i^∨⟩) and φ i (x₁, x₂) = max (φ i x₂) (φ i x₁ + ⟨wt x₂, α_i^∨⟩); see TauCeti.NormalCrystal.tensor_ε_eq_max and TauCeti.NormalCrystal.tensor_φ_eq_max.

Main definitions

• TauCeti.NormalCrystal.tensor: the tensor product of two normal crystals.
• TauCeti.NormalCrystal.StrictHom.tensor: the tensor product of two strict morphisms.
• TauCeti.NormalCrystal.tensorAssoc, TauCeti.NormalCrystal.tensorAssocInv: the associator (B₁ ⊗ B₂) ⊗ B₃ → B₁ ⊗ (B₂ ⊗ B₃) and its inverse, as strict morphisms.
• TauCeti.NormalCrystal.dualTensor, TauCeti.NormalCrystal.dualTensorInv: the strict morphism (B₁ ⊗ B₂)^∨ → B₂^∨ ⊗ B₁^∨ exchanging the factors, and its inverse.

Main results

• TauCeti.NormalCrystal.tensor_e_of_le, TauCeti.NormalCrystal.tensor_e_of_lt, TauCeti.NormalCrystal.tensor_f_of_lt, TauCeti.NormalCrystal.tensor_f_of_le: the tensor product rule on each side of the tie.
• TauCeti.NormalCrystal.StrictHom.tensor_id, TauCeti.NormalCrystal.StrictHom.tensor_comp: functoriality of the tensor product in strict morphisms.
• TauCeti.NormalCrystal.tensorAssocInv_comp_tensorAssoc, TauCeti.NormalCrystal.tensorAssoc_comp_tensorAssocInv: associativity of the tensor product up to strict isomorphism.
• TauCeti.NormalCrystal.dualTensorInv_comp_dualTensor, TauCeti.NormalCrystal.dualTensor_comp_dualTensorInv: (B₁ ⊗ B₂)^∨ ≅ B₂^∨ ⊗ B₁^∨.

References

• M. Kashiwara, On crystal bases, CMS Conf. Proc. 16 (1995), §7.
• P. Littelmann, Paths and root operators in representation theory, Ann. of Math. 142 (1995), §2.
• D. Bump and A. Schilling, Crystal bases: representations and combinatorics, World Scientific (2017), Ch. 2.

def TauCeti.NormalCrystal.tensor {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) : NormalCrystal P b (B₁ × B₂)

The tensor product B₁ ⊗ B₂ of two normal crystals, on the product type, with Kashiwara's tie convention: on a tie φ i x₁ = ε i x₂ the raising operator acts on the left factor and the lowering operator on the right factor.

@[simp]

theorem TauCeti.NormalCrystal.tensor_wt {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} (x : B₁ × B₂) : (c.tensor d).wt x = c.wt x.1 + d.wt x.2

@[simp]

theorem TauCeti.NormalCrystal.tensor_ε {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} (i : ↥b.support) (x : B₁ × B₂) : (c.tensor d).ε i x = c.ε i x.1 + (d.ε i x.2 - c.φ i x.1)

@[simp]

theorem TauCeti.NormalCrystal.tensor_φ {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} (i : ↥b.support) (x : B₁ × B₂) : (c.tensor d).φ i x = d.φ i x.2 + (c.φ i x.1 - d.ε i x.2)

theorem TauCeti.NormalCrystal.tensor_e {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} (i : ↥b.support) (x : B₁ × B₂) : (c.tensor d).e i x = if d.ε i x.2 ≤ c.φ i x.1 then Option.map (fun (x_1 : B₁) => (x_1, x.2)) (c.e i x.1) else Option.map (fun (x_1 : B₂) => (x.1, x_1)) (d.e i x.2)

theorem TauCeti.NormalCrystal.tensor_f {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} (i : ↥b.support) (x : B₁ × B₂) : (c.tensor d).f i x = if d.ε i x.2 < c.φ i x.1 then Option.map (fun (x_1 : B₁) => (x_1, x.2)) (c.f i x.1) else Option.map (fun (x_1 : B₂) => (x.1, x_1)) (d.f i x.2)

@[simp]

theorem TauCeti.NormalCrystal.tensor_e_of_le {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} {i : ↥b.support} {x₁ : B₁} {x₂ : B₂} (h : d.ε i x₂ ≤ c.φ i x₁) : (c.tensor d).e i (x₁, x₂) = Option.map (fun (x : B₁) => (x, x₂)) (c.e i x₁)

The tensor product rule for raising, when it acts on the left factor (including the tie).

@[simp]

theorem TauCeti.NormalCrystal.tensor_e_of_lt {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} {i : ↥b.support} {x₁ : B₁} {x₂ : B₂} (h : c.φ i x₁ < d.ε i x₂) : (c.tensor d).e i (x₁, x₂) = Option.map (fun (x : B₂) => (x₁, x)) (d.e i x₂)

The tensor product rule for raising, when it acts on the right factor.

@[simp]

theorem TauCeti.NormalCrystal.tensor_f_of_lt {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} {i : ↥b.support} {x₁ : B₁} {x₂ : B₂} (h : d.ε i x₂ < c.φ i x₁) : (c.tensor d).f i (x₁, x₂) = Option.map (fun (x : B₁) => (x, x₂)) (c.f i x₁)

The tensor product rule for lowering, when it acts on the left factor.

@[simp]

theorem TauCeti.NormalCrystal.tensor_f_of_le {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} {i : ↥b.support} {x₁ : B₁} {x₂ : B₂} (h : c.φ i x₁ ≤ d.ε i x₂) : (c.tensor d).f i (x₁, x₂) = Option.map (fun (x : B₂) => (x₁, x)) (d.f i x₂)

The tensor product rule for lowering, when it acts on the right factor (including the tie).

theorem TauCeti.NormalCrystal.tensor_ε_eq_max {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} (i : ↥b.support) (x : B₁ × B₂) : ↑((c.tensor d).ε i x) = max (↑(c.ε i x.1)) (↑(d.ε i x.2) - (P.toLinearMap (c.wt x.1)) (P.coroot ↑i))

Kashiwara's form of the raising string length of a tensor product: ε i (x₁ ⊗ x₂) = max (ε i x₁) (ε i x₂ - ⟨wt x₁, α_i^∨⟩).

theorem TauCeti.NormalCrystal.tensor_φ_eq_max {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₂} (i : ↥b.support) (x : B₁ × B₂) : ↑((c.tensor d).φ i x) = max (↑(d.φ i x.2)) (↑(c.φ i x.1) + (P.toLinearMap (d.wt x.2)) (P.coroot ↑i))

Kashiwara's form of the lowering string length of a tensor product: φ i (x₁ ⊗ x₂) = max (φ i x₂) (φ i x₁ + ⟨wt x₂, α_i^∨⟩).

Functoriality

def TauCeti.NormalCrystal.StrictHom.tensor {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {B₄ : Type x₄} {B₅ : Type x₅} {c : NormalCrystal P b B₁} {c' : NormalCrystal P b B₂} {d : NormalCrystal P b B₄} {d' : NormalCrystal P b B₅} (ψ : c.StrictHom c') (χ : d.StrictHom d') : (c.tensor d).StrictHom (c'.tensor d')

The tensor product ψ ⊗ χ of two strict morphisms, acting factorwise.

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.tensor_apply {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {B₄ : Type x₄} {B₅ : Type x₅} {c : NormalCrystal P b B₁} {c' : NormalCrystal P b B₂} {d : NormalCrystal P b B₄} {d' : NormalCrystal P b B₅} (ψ : c.StrictHom c') (χ : d.StrictHom d') (x : B₁ × B₄) : (ψ.tensor χ) x = (ψ x.1, χ x.2)

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.tensor_id {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₄ : Type x₄} {c : NormalCrystal P b B₁} {d : NormalCrystal P b B₄} : (id c).tensor (id d) = id (c.tensor d)

theorem TauCeti.NormalCrystal.StrictHom.tensor_comp {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {B₃ : Type x₃} {B₄ : Type x₄} {B₅ : Type x₅} {B₆ : Type x₆} {c : NormalCrystal P b B₁} {c' : NormalCrystal P b B₂} {c'' : NormalCrystal P b B₃} {d : NormalCrystal P b B₄} {d' : NormalCrystal P b B₅} {d'' : NormalCrystal P b B₆} (ψ : c.StrictHom c') (ψ' : c'.StrictHom c'') (χ : d.StrictHom d') (χ' : d'.StrictHom d'') : (ψ'.comp ψ).tensor (χ'.comp χ) = (ψ'.tensor χ').comp (ψ.tensor χ)

Associativity

def TauCeti.NormalCrystal.tensorAssoc {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {B₃ : Type x₃} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) (g : NormalCrystal P b B₃) : ((c.tensor d).tensor g).StrictHom (c.tensor (d.tensor g))

The associator (B₁ ⊗ B₂) ⊗ B₃ → B₁ ⊗ (B₂ ⊗ B₃) of the tensor product, a strict morphism with inverse TauCeti.NormalCrystal.tensorAssocInv.

def TauCeti.NormalCrystal.tensorAssocInv {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {B₃ : Type x₃} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) (g : NormalCrystal P b B₃) : (c.tensor (d.tensor g)).StrictHom ((c.tensor d).tensor g)

The inverse B₁ ⊗ (B₂ ⊗ B₃) → (B₁ ⊗ B₂) ⊗ B₃ of the associator TauCeti.NormalCrystal.tensorAssoc.

@[simp]

theorem TauCeti.NormalCrystal.tensorAssoc_apply {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {B₃ : Type x₃} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) (g : NormalCrystal P b B₃) (x : (B₁ × B₂) × B₃) : (c.tensorAssoc d g) x = (x.1.1, x.1.2, x.2)

@[simp]

theorem TauCeti.NormalCrystal.tensorAssocInv_apply {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {B₃ : Type x₃} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) (g : NormalCrystal P b B₃) (x : B₁ × B₂ × B₃) : (c.tensorAssocInv d g) x = ((x.1, x.2.1), x.2.2)

@[simp]

theorem TauCeti.NormalCrystal.tensorAssocInv_comp_tensorAssoc {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {B₃ : Type x₃} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) (g : NormalCrystal P b B₃) : (c.tensorAssocInv d g).comp (c.tensorAssoc d g) = StrictHom.id ((c.tensor d).tensor g)

@[simp]

theorem TauCeti.NormalCrystal.tensorAssoc_comp_tensorAssocInv {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} {B₃ : Type x₃} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) (g : NormalCrystal P b B₃) : (c.tensorAssoc d g).comp (c.tensorAssocInv d g) = StrictHom.id (c.tensor (d.tensor g))

Duality

def TauCeti.NormalCrystal.dualTensor {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) : (c.tensor d).dual.StrictHom (d.dual.tensor c.dual)

The strict morphism (B₁ ⊗ B₂)^∨ → B₂^∨ ⊗ B₁^∨ exchanging the two factors, with inverse TauCeti.NormalCrystal.dualTensorInv. Duality exchanges the two halves of the tie convention: on a tie the lowering operator of B₁ ⊗ B₂ acts on its right factor, which is the left factor of B₂^∨ ⊗ B₁^∨, where raising acts on ties.

def TauCeti.NormalCrystal.dualTensorInv {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) : (d.dual.tensor c.dual).StrictHom (c.tensor d).dual

The inverse B₂^∨ ⊗ B₁^∨ → (B₁ ⊗ B₂)^∨ of TauCeti.NormalCrystal.dualTensor.

@[simp]

theorem TauCeti.NormalCrystal.dualTensor_apply {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) (x : B₁ × B₂) : (c.dualTensor d) x = x.swap

@[simp]

theorem TauCeti.NormalCrystal.dualTensorInv_apply {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) (x : B₂ × B₁) : (c.dualTensorInv d) x = x.swap

@[simp]

theorem TauCeti.NormalCrystal.dualTensorInv_comp_dualTensor {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) : (c.dualTensorInv d).comp (c.dualTensor d) = StrictHom.id (c.tensor d).dual

@[simp]

theorem TauCeti.NormalCrystal.dualTensor_comp_dualTensorInv {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁} {B₂ : Type x₂} (c : NormalCrystal P b B₁) (d : NormalCrystal P b B₂) : (c.dualTensor d).comp (c.dualTensorInv d) = StrictHom.id (d.dual.tensor c.dual)