Normal crystals over a root datum

Fix a root datum P : RootDatum ι X Y with a base b, so that the simple roots are the P.root i and the simple coroots the P.coroot i for i : b.support. A normal crystal over (P, b) is a type B with a weight map wt : B → X, raising and lowering operators e i, f i : B → Option B (with none playing the role of Kashiwara's 0) and natural numbers ε i x, φ i x such that

• f i and e i are partial inverses: f i x = some y ↔ e i y = some x;
• raising adds the simple root to the weight and lowers ε i by one;
• ε i x is the length of the e i-string above x and φ i x that of the f i-string below it, which is encoded by ε i x = 0 ↔ e i x = none, φ i x = 0 ↔ f i x = none and the shift of ε i along e i;
• φ i x - ε i x = ⟨wt x, α_i^∨⟩.

These are Kashiwara's crystal axioms together with his seminormality condition, which Joseph and the path-model literature call normality; since ε i and φ i are natural numbers every string is finite. Crystals of Littelmann paths and of integrable highest weight modules are of this kind.

The structure records ε and φ as data, but TauCeti.NormalCrystal.ext shows that a normal crystal is determined by its weight map and its raising operators: the lowering operators and the string lengths carry no further freedom.

Main definitions

• TauCeti.NormalCrystal: a normal crystal over a root datum with a base.
• TauCeti.NormalCrystal.dual: the dual crystal, exchanging e with f, ε with φ and negating the weight.
• TauCeti.NormalCrystal.eIter, TauCeti.NormalCrystal.fIter: iterated root operators.
• TauCeti.NormalCrystal.StrictHom: strict morphisms of normal crystals that are defined everywhere (no element is sent to 0), with identities, composition and duals.
• TauCeti.NormalCrystal.StrictIso: strict isomorphisms of normal crystals, with inverses, composition and duals.
• TauCeti.NormalCrystal.transport: the transport of a normal crystal along a bijection of the underlying types, with the strict isomorphism TauCeti.NormalCrystal.transportIso.

Main results

• TauCeti.NormalCrystal.ext: a normal crystal is determined by wt and e.
• TauCeti.NormalCrystal.e_ne_some_self, TauCeti.NormalCrystal.f_ne_some_self: no root operator fixes an element.
• TauCeti.NormalCrystal.isSome_eIter_iff, TauCeti.NormalCrystal.isSome_fIter_iff: the string identities e i ^ n x ≠ 0 ↔ n ≤ ε i x and f i ^ n x ≠ 0 ↔ n ≤ φ i x, with the weight and string-length changes TauCeti.NormalCrystal.wt_of_eIter_eq_some, TauCeti.NormalCrystal.ε_of_eIter_eq_some and their lowering counterparts.
• TauCeti.NormalCrystal.StrictHom.ε_apply, TauCeti.NormalCrystal.StrictHom.φ_apply, TauCeti.NormalCrystal.StrictHom.f_apply: a map preserving weights and commuting with the raising operators preserves the string lengths and commutes with the lowering operators.
• TauCeti.NormalCrystal.StrictIso.eq_transport: the target of a strict isomorphism is the transport of its source along the underlying bijection.

References

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

structure TauCeti.NormalCrystal {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] (P : RootDatum ι X Y) (b : RootPairing.Base P) (B : Type x₁) : Type (max (max u v) x₁)

A normal crystal over the root datum P with base b: a weight map, partial raising and lowering operators e i, f i indexed by the simple roots, and natural string lengths ε i, φ i, satisfying Kashiwara's crystal axioms together with normality (ε i x and φ i x are the lengths of the e i- and f i-strings through x). The value none of e i or f i stands for Kashiwara's 0.

• wt : B → X

  The weight map.

• e : ↥b.support → B → Option B

  The raising operator attached to a simple root.

• f : ↥b.support → B → Option B

  The lowering operator attached to a simple root.

• ε : ↥b.support → B → ℕ

  The length of the raising string above an element.

• φ : ↥b.support → B → ℕ

  The length of the lowering string below an element.

• f_eq_some_iff {i : ↥b.support} {x y : B} : self.f i x = some y ↔ self.e i y = some x

  Lowering and raising are partial inverses.

• wt_of_e_eq_some {i : ↥b.support} {x y : B} : self.e i x = some y → self.wt y = self.wt x + P.root ↑i

  Raising adds the simple root to the weight.

• ε_eq_zero_iff {i : ↥b.support} {x : B} : self.ε i x = 0 ↔ self.e i x = none

  The raising string above x is empty exactly when e i x is undefined.

• ε_of_e_eq_some {i : ↥b.support} {x y : B} : self.e i x = some y → self.ε i y + 1 = self.ε i x

  Raising shortens the raising string by one.

• φ_eq_zero_iff {i : ↥b.support} {x : B} : self.φ i x = 0 ↔ self.f i x = none

  The lowering string below x is empty exactly when f i x is undefined.

• φ_sub_ε (i : ↥b.support) (x : B) : ↑(self.φ i x) - ↑(self.ε i x) = (P.toLinearMap (self.wt x)) (P.coroot ↑i)

  The difference of the string lengths is the pairing of the weight with the coroot.

theorem TauCeti.NormalCrystal.e_eq_some_iff {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {x y : B} : c.e i x = some y ↔ c.f i y = some x

theorem TauCeti.NormalCrystal.e_ne_none_iff {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {x : B} : c.e i x ≠ none ↔ c.ε i x ≠ 0

theorem TauCeti.NormalCrystal.f_ne_none_iff {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {x : B} : c.f i x ≠ none ↔ c.φ i x ≠ 0

theorem TauCeti.NormalCrystal.wt_of_f_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {x y : B} (h : c.f i x = some y) : c.wt y = c.wt x - P.root ↑i

Lowering subtracts the simple root from the weight.

theorem TauCeti.NormalCrystal.e_ne_some_self {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {x : B} : c.e i x ≠ some x

No raising operator fixes an element, since it changes the weight by a simple root.

theorem TauCeti.NormalCrystal.f_ne_some_self {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {x : B} : c.f i x ≠ some x

No lowering operator fixes an element.

theorem TauCeti.NormalCrystal.ε_of_f_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {x y : B} (h : c.f i x = some y) : c.ε i y = c.ε i x + 1

Lowering lengthens the raising string by one.

theorem TauCeti.NormalCrystal.φ_of_e_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {x y : B} (h : c.e i x = some y) : c.φ i y = c.φ i x + 1

Raising lengthens the lowering string by one.

theorem TauCeti.NormalCrystal.φ_of_f_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {x y : B} (h : c.f i x = some y) : c.φ i y + 1 = c.φ i x

Lowering shortens the lowering string by one.

theorem TauCeti.NormalCrystal.ε_apply_eq_of_e_map {ι : 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) {i : ↥b.support} (d : NormalCrystal P b B') {g : B → B'} (hg : ∀ (x : B), d.e i (g x) = Option.map g (c.e i x)) (x : B) : d.ε i (g x) = c.ε i x

A map commuting with the raising operators preserves the lengths of raising strings.

theorem TauCeti.NormalCrystal.φ_apply_eq_of_e_map {ι : 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) {i : ↥b.support} (d : NormalCrystal P b B') {g : B → B'} (x : B) (hwt : d.wt (g x) = c.wt x) (hg : ∀ (x : B), d.e i (g x) = Option.map g (c.e i x)) : d.φ i (g x) = c.φ i x

A map commuting with the raising operators preserves the lengths of lowering strings at every point where it preserves the weight.

theorem TauCeti.NormalCrystal.f_apply_eq_of_e_map {ι : 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) {i : ↥b.support} (d : NormalCrystal P b B') {g : B → B'} (x : B) (hwt : d.wt (g x) = c.wt x) (hg : ∀ (x : B), d.e i (g x) = Option.map g (c.e i x)) : d.f i (g x) = Option.map g (c.f i x)

A map commuting with the raising operators commutes with the lowering operators at every point where it preserves the weight.

theorem TauCeti.NormalCrystal.ext {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} {c d : NormalCrystal P b B} (hwt : c.wt = d.wt) (he : c.e = d.e) : c = d

A normal crystal is determined by its weight map and its raising operators.

theorem TauCeti.NormalCrystal.ext_iff {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} {c d : NormalCrystal P b B} : c = d ↔ c.wt = d.wt ∧ c.e = d.e

The dual crystal

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

The dual crystal: the same underlying type with the raising and lowering operators and the two string lengths exchanged and the weight negated.

@[simp]

theorem TauCeti.NormalCrystal.dual_wt {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) (x : B) : c.dual.wt x = -c.wt x

@[simp]

theorem TauCeti.NormalCrystal.dual_e {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) : c.dual.e = c.f

@[simp]

theorem TauCeti.NormalCrystal.dual_f {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) : c.dual.f = c.e

@[simp]

theorem TauCeti.NormalCrystal.dual_ε {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) : c.dual.ε = c.φ

@[simp]

theorem TauCeti.NormalCrystal.dual_φ {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) : c.dual.φ = c.ε

@[simp]

theorem TauCeti.NormalCrystal.dual_dual {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) : c.dual.dual = c

Strings

def TauCeti.NormalCrystal.eIter {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) (i : ↥b.support) : ℕ → B → Option B

The n-fold raising operator e i ^ n, as a partial map.

def TauCeti.NormalCrystal.fIter {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) (i : ↥b.support) : ℕ → B → Option B

The n-fold lowering operator f i ^ n, as a partial map.

@[simp]

theorem TauCeti.NormalCrystal.eIter_zero {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} (x : B) : c.eIter i 0 x = some x

theorem TauCeti.NormalCrystal.eIter_succ {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} (n : ℕ) (x : B) : c.eIter i (n + 1) x = (c.e i x).bind (c.eIter i n)

@[simp]

theorem TauCeti.NormalCrystal.fIter_zero {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} (x : B) : c.fIter i 0 x = some x

theorem TauCeti.NormalCrystal.fIter_succ {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} (n : ℕ) (x : B) : c.fIter i (n + 1) x = (c.f i x).bind (c.fIter i n)

@[simp]

theorem TauCeti.NormalCrystal.eIter_one {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} (x : B) : c.eIter i 1 x = c.e i x

@[simp]

theorem TauCeti.NormalCrystal.fIter_one {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} (x : B) : c.fIter i 1 x = c.f i x

theorem TauCeti.NormalCrystal.eIter_succ' {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} (n : ℕ) (x : B) : c.eIter i (n + 1) x = (c.eIter i n x).bind (c.e i)

@[simp]

theorem TauCeti.NormalCrystal.dual_eIter {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) : c.dual.eIter = c.fIter

@[simp]

theorem TauCeti.NormalCrystal.dual_fIter {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) : c.dual.fIter = c.eIter

theorem TauCeti.NormalCrystal.fIter_succ' {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} (n : ℕ) (x : B) : c.fIter i (n + 1) x = (c.fIter i n x).bind (c.f i)

theorem TauCeti.NormalCrystal.wt_of_eIter_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x y : B} (h : c.eIter i n x = some y) : c.wt y = c.wt x + n • P.root ↑i

Raising n times adds n copies of the simple root to the weight.

theorem TauCeti.NormalCrystal.ε_of_eIter_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x y : B} (h : c.eIter i n x = some y) : c.ε i y + n = c.ε i x

Raising n times shortens the raising string by n.

@[simp]

theorem TauCeti.NormalCrystal.isSome_eIter_iff {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x : B} : (c.eIter i n x).isSome = true ↔ n ≤ c.ε i x

String identity for raising: e i ^ n x is defined exactly when n ≤ ε i x.

@[simp]

theorem TauCeti.NormalCrystal.eIter_eq_none_iff {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x : B} : c.eIter i n x = none ↔ c.ε i x < n

theorem TauCeti.NormalCrystal.wt_of_fIter_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x y : B} (h : c.fIter i n x = some y) : c.wt y = c.wt x - n • P.root ↑i

Lowering n times subtracts n copies of the simple root from the weight.

theorem TauCeti.NormalCrystal.φ_of_fIter_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x y : B} (h : c.fIter i n x = some y) : c.φ i y + n = c.φ i x

Lowering n times shortens the lowering string by n.

@[simp]

theorem TauCeti.NormalCrystal.isSome_fIter_iff {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x : B} : (c.fIter i n x).isSome = true ↔ n ≤ c.φ i x

String identity for lowering: f i ^ n x is defined exactly when n ≤ φ i x.

@[simp]

theorem TauCeti.NormalCrystal.fIter_eq_none_iff {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x : B} : c.fIter i n x = none ↔ c.φ i x < n

theorem TauCeti.NormalCrystal.fIter_eq_some_iff {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x y : B} : c.fIter i n x = some y ↔ c.eIter i n y = some x

The iterated root operators are partial inverses of each other.

theorem TauCeti.NormalCrystal.ε_of_fIter_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x y : B} (h : c.fIter i n x = some y) : c.ε i y = c.ε i x + n

Lowering n times lengthens the raising string by n.

theorem TauCeti.NormalCrystal.φ_of_eIter_eq_some {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} (c : NormalCrystal P b B) {i : ↥b.support} {n : ℕ} {x y : B} (h : c.eIter i n x = some y) : c.φ i y = c.φ i x + n

Raising n times lengthens the lowering string by n.

Strict morphisms

structure TauCeti.NormalCrystal.StrictHom {ι : 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') : Type (max x₁ x₂)

A strict morphism of normal crystals: a map of the underlying types preserving weights and commuting with the raising operators. It then also preserves the string lengths and commutes with the lowering operators (TauCeti.NormalCrystal.StrictHom.ε_apply, TauCeti.NormalCrystal.StrictHom.φ_apply, TauCeti.NormalCrystal.StrictHom.f_apply).

This is a total map B → B'. Kashiwara's strict morphisms are maps B ⊔ {0} → B' ⊔ {0} fixing 0, which may also send elements, even whole connected components, to 0; StrictHom is the case in which no element is sent to 0. For isomorphisms (TauCeti.NormalCrystal.StrictIso) the two conventions agree.

• toFun : B → B'

  The underlying map.

• wt_toFun (x : B) : d.wt (self.toFun x) = c.wt x

  A strict morphism preserves weights.

• e_toFun (i : ↥b.support) (x : B) : d.e i (self.toFun x) = Option.map self.toFun (c.e i x)

  A strict morphism commutes with the raising operators.

@[instance_reducible]

instance TauCeti.NormalCrystal.StrictHom.instFunLike {ι : 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'} : FunLike (c.StrictHom d) B B'

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.toFun_eq_coe {ι : 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.StrictHom d) : ψ.toFun = ⇑ψ

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.coe_mk {ι : 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'} (g : B → B') (hwt : ∀ (x : B), d.wt (g x) = c.wt x) (he : ∀ (i : ↥b.support) (x : B), d.e i (g x) = Option.map g (c.e i x)) : ⇑{ toFun := g, wt_toFun := hwt, e_toFun := he } = g

theorem TauCeti.NormalCrystal.StrictHom.ext {ι : 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.StrictHom d} (h : ∀ (x : B), ψ x = χ x) : ψ = χ

theorem TauCeti.NormalCrystal.StrictHom.ext_iff {ι : 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.StrictHom d} : ψ = χ ↔ ∀ (x : B), ψ x = χ x

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.wt_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'} (ψ : c.StrictHom d) (x : B) : d.wt (ψ x) = c.wt x

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.e_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'} (ψ : c.StrictHom d) (i : ↥b.support) (x : B) : d.e i (ψ x) = Option.map (⇑ψ) (c.e i x)

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.ε_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'} (ψ : c.StrictHom d) (i : ↥b.support) (x : B) : d.ε i (ψ x) = c.ε i x

A strict morphism preserves the string lengths ε i.

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.φ_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'} (ψ : c.StrictHom d) (i : ↥b.support) (x : B) : d.φ i (ψ x) = c.φ i x

A strict morphism preserves the string lengths φ i.

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.f_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'} (ψ : c.StrictHom d) (i : ↥b.support) (x : B) : d.f i (ψ x) = Option.map (⇑ψ) (c.f i x)

A strict morphism commutes with the lowering operators.

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.eIter_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'} (ψ : c.StrictHom d) (i : ↥b.support) (x : B) (n : ℕ) : d.eIter i n (ψ x) = Option.map (⇑ψ) (c.eIter i n x)

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.fIter_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'} (ψ : c.StrictHom d) (i : ↥b.support) (x : B) (n : ℕ) : d.fIter i n (ψ x) = Option.map (⇑ψ) (c.fIter i n x)

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

The identity strict morphism.

@[simp]

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

def TauCeti.NormalCrystal.StrictHom.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₃} {c : NormalCrystal P b B} {d : NormalCrystal P b B'} {d' : NormalCrystal P b B''} (χ : d.StrictHom d') (ψ : c.StrictHom d) : c.StrictHom d'

Composition of strict morphisms.

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.comp_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'} {d' : NormalCrystal P b B''} (ψ : c.StrictHom d) (x : B) (χ : d.StrictHom d') : (χ.comp ψ) x = χ (ψ x)

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.comp_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'} (ψ : c.StrictHom d) : ψ.comp (id c) = ψ

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.id_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₂} {c : NormalCrystal P b B} {d : NormalCrystal P b B'} (ψ : c.StrictHom d) : (id d).comp ψ = ψ

theorem TauCeti.NormalCrystal.StrictHom.comp_assoc {ι : 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'} {d' : NormalCrystal P b B''} (ψ : c.StrictHom d) {B''' : Type u_1} {d'' : NormalCrystal P b B'''} (θ : d'.StrictHom d'') (χ : d.StrictHom d') : (θ.comp χ).comp ψ = θ.comp (χ.comp ψ)

def TauCeti.NormalCrystal.StrictHom.dual {ι : 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.StrictHom d) : c.dual.StrictHom d.dual

A strict morphism is also a strict morphism between the dual crystals.

@[simp]

theorem TauCeti.NormalCrystal.StrictHom.dual_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'} (ψ : c.StrictHom d) (x : B) : ψ.dual x = ψ x

Strict isomorphisms and transport

structure TauCeti.NormalCrystal.StrictIso {ι : 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') extends B ≃ B' : Type (max x₁ x₂)

A strict isomorphism of normal crystals: a bijection of the underlying types preserving weights and commuting with the raising operators. Its inverse is again a strict isomorphism (TauCeti.NormalCrystal.StrictIso.symm).

• toFun : B → B'
• invFun : B' → B
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• wt_toFun (x : B) : d.wt (self.toFun x) = c.wt x

  A strict isomorphism preserves weights.

• e_toFun (i : ↥b.support) (x : B) : d.e i (self.toFun x) = Option.map self.toFun (c.e i x)

  A strict isomorphism commutes with the raising operators.

@[instance_reducible]

instance TauCeti.NormalCrystal.StrictIso.instEquivLike {ι : 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'} : EquivLike (c.StrictIso d) B B'

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.coe_toEquiv {ι : 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.StrictIso d) : ⇑ψ.toEquiv = ⇑ψ

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.coe_mk {ι : 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'} (g : B ≃ B') (hwt : ∀ (x : B), d.wt (g.toFun x) = c.wt x) (he : ∀ (i : ↥b.support) (x : B), d.e i (g.toFun x) = Option.map g.toFun (c.e i x)) : ⇑{ toEquiv := g, wt_toFun := hwt, e_toFun := he } = ⇑g

theorem TauCeti.NormalCrystal.StrictIso.ext {ι : 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.StrictIso d} (h : ∀ (x : B), ψ x = χ x) : ψ = χ

theorem TauCeti.NormalCrystal.StrictIso.ext_iff {ι : 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.StrictIso d} : ψ = χ ↔ ∀ (x : B), ψ x = χ x

def TauCeti.NormalCrystal.StrictIso.toStrictHom {ι : 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.StrictIso d) : c.StrictHom d

The strict morphism underlying a strict isomorphism.

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.coe_toStrictHom {ι : 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.StrictIso d) : ⇑ψ.toStrictHom = ⇑ψ

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.wt_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'} (ψ : c.StrictIso d) (x : B) : d.wt (ψ x) = c.wt x

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.e_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'} (ψ : c.StrictIso d) (i : ↥b.support) (x : B) : d.e i (ψ x) = Option.map (⇑ψ) (c.e i x)

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.ε_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'} (ψ : c.StrictIso d) (i : ↥b.support) (x : B) : d.ε i (ψ x) = c.ε i x

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.φ_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'} (ψ : c.StrictIso d) (i : ↥b.support) (x : B) : d.φ i (ψ x) = c.φ i x

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.f_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'} (ψ : c.StrictIso d) (i : ↥b.support) (x : B) : d.f i (ψ x) = Option.map (⇑ψ) (c.f i x)

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

The identity strict isomorphism.

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.refl_apply {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B : Type x₁} {c : NormalCrystal P b B} (x : B) : (refl c) x = x

def TauCeti.NormalCrystal.StrictIso.symm {ι : 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.StrictIso d) : d.StrictIso c

The inverse of a strict isomorphism.

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.toEquiv_symm {ι : 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.StrictIso d) : ψ.symm.toEquiv = ψ.symm

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.coe_toEquiv_symm {ι : 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.StrictIso d) : ⇑ψ.symm = ⇑ψ.symm

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.symm_apply_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'} (ψ : c.StrictIso d) (x : B) : ψ.symm (ψ x) = x

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.apply_symm_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'} (ψ : c.StrictIso d) (y : B') : ψ (ψ.symm y) = y

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.symm_symm {ι : 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.StrictIso d) : ψ.symm.symm = ψ

def TauCeti.NormalCrystal.StrictIso.trans {ι : 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'} {d' : NormalCrystal P b B''} (ψ : c.StrictIso d) (χ : d.StrictIso d') : c.StrictIso d'

Composition of strict isomorphisms.

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.trans_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'} {d' : NormalCrystal P b B''} (ψ : c.StrictIso d) (x : B) (χ : d.StrictIso d') : (ψ.trans χ) x = χ (ψ x)

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.self_trans_symm {ι : 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.StrictIso d) : ψ.trans ψ.symm = refl c

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.symm_trans_self {ι : 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.StrictIso d) : ψ.symm.trans ψ = refl d

noncomputable def TauCeti.NormalCrystal.StrictIso.ofBijective {ι : 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.StrictHom d) (h : Function.Bijective ⇑ψ) : c.StrictIso d

A bijective strict morphism is a strict isomorphism.

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.coe_ofBijective {ι : 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.StrictHom d) (h : Function.Bijective ⇑ψ) : ⇑(ofBijective ψ h) = ⇑ψ

def TauCeti.NormalCrystal.StrictIso.dual {ι : 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.StrictIso d) : c.dual.StrictIso d.dual

A strict isomorphism is also a strict isomorphism between the dual crystals.

@[simp]

theorem TauCeti.NormalCrystal.StrictIso.dual_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'} (ψ : c.StrictIso d) (x : B) : ψ.dual x = ψ x

def TauCeti.NormalCrystal.transport {ι : 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) (σ : B ≃ B') : NormalCrystal P b B'

The transport of a normal crystal along a bijection σ : B ≃ B': the normal crystal on B' for which σ is a strict isomorphism (TauCeti.NormalCrystal.transportIso).

@[simp]

theorem TauCeti.NormalCrystal.transport_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) (σ : B ≃ B') (y : B') : (c.transport σ).wt y = c.wt (σ.symm y)

@[simp]

theorem TauCeti.NormalCrystal.transport_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) (σ : B ≃ B') (i : ↥b.support) (y : B') : (c.transport σ).e i y = Option.map (⇑σ) (c.e i (σ.symm y))

@[simp]

theorem TauCeti.NormalCrystal.transport_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) (σ : B ≃ B') (i : ↥b.support) (y : B') : (c.transport σ).f i y = Option.map (⇑σ) (c.f i (σ.symm y))

@[simp]

theorem TauCeti.NormalCrystal.transport_ε {ι : 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) (σ : B ≃ B') (i : ↥b.support) (y : B') : (c.transport σ).ε i y = c.ε i (σ.symm y)

@[simp]

theorem TauCeti.NormalCrystal.transport_φ {ι : 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) (σ : B ≃ B') (i : ↥b.support) (y : B') : (c.transport σ).φ i y = c.φ i (σ.symm y)

def TauCeti.NormalCrystal.transportIso {ι : 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) (σ : B ≃ B') : c.StrictIso (c.transport σ)

The bijection σ as a strict isomorphism onto the transported crystal.

@[simp]

theorem TauCeti.NormalCrystal.coe_transportIso {ι : 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) (σ : B ≃ B') : ⇑(c.transportIso σ) = ⇑σ

theorem TauCeti.NormalCrystal.StrictIso.eq_transport {ι : 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.StrictIso d) : d = c.transport ψ.toEquiv

Uniqueness of transport: the target of a strict isomorphism is the transport of its source along the underlying bijection.