Trees

In this file, we define the types of trees of a given type τ. For each type index α, an α-tree of τ is a function from α-extended type indices to τ. This will be used to define structural permutations (along with many more gadgets).

If τ has a group structure, the α-trees of τ can also be given a group structure by "branchwise" multiplication.

Main declarations

• ConNF.Tree: The type of trees of a given type τ.
• ConNF.Tree.group: The group structure on trees.
• ConNF.Tree.comp: The derivative functor on tree groups.

def ConNF.Tree [ConNF.Params] (τ : Type u) (α : ConNF.TypeIndex) : Type u

For each type index α, an α-tree of τ is a function from α-extended type indices to τ.

Equations

• ConNF.Tree τ α = (ConNF.ExtendedIndex α → τ)

def ConNF.Tree.toBot [ConNF.Params] {τ : Type u} : τ ≃ ConNF.Tree τ ⊥

The equivalence between τ and Tree τ ⊥.

Equations

• ConNF.Tree.toBot = { toFun := fun (a : τ) (x : ConNF.ExtendedIndex ⊥) => a, invFun := fun (a : ConNF.Tree τ ⊥) => a Quiver.Path.nil, left_inv := ⋯, right_inv := ⋯ }

def ConNF.Tree.ofBot [ConNF.Params] {τ : Type u} : ConNF.Tree τ ⊥ ≃ τ

The equivalence between Tree τ ⊥ and τ.

Equations

• ConNF.Tree.ofBot = { toFun := fun (a : ConNF.Tree τ ⊥) => a Quiver.Path.nil, invFun := fun (a : τ) (x : ConNF.ExtendedIndex ⊥) => a, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem ConNF.Tree.toBot_symm [ConNF.Params] {τ : Type u} : ConNF.Tree.toBot.symm = ConNF.Tree.ofBot

@[simp]

theorem ConNF.Tree.ofBot_symm [ConNF.Params] {τ : Type u} : ConNF.Tree.ofBot.symm = ConNF.Tree.toBot

@[simp]

theorem ConNF.Tree.toBot_ofBot [ConNF.Params] {τ : Type u} (a : ConNF.Tree τ ⊥) : ConNF.Tree.toBot (ConNF.Tree.ofBot a) = a

@[simp]

theorem ConNF.Tree.ofBot_toBot [ConNF.Params] {τ : Type u} (a : τ) : ConNF.Tree.ofBot (ConNF.Tree.toBot a) = a

@[simp]

theorem ConNF.Tree.toBot_inj [ConNF.Params] {τ : Type u} {a : τ} {b : τ} : ConNF.Tree.toBot a = ConNF.Tree.toBot b ↔ a = b

@[simp]

theorem ConNF.Tree.ofBot_inj [ConNF.Params] {τ : Type u} {a : ConNF.Tree τ ⊥} {b : ConNF.Tree τ ⊥} : ConNF.Tree.ofBot a = ConNF.Tree.ofBot b ↔ a = b

theorem ConNF.Tree.ext [ConNF.Params] {τ : Type u} {α : ConNF.TypeIndex} (a : ConNF.Tree τ α) (b : ConNF.Tree τ α) (h : ∀ (A : ConNF.ExtendedIndex α), a A = b A) : a = b

instance ConNF.Tree.group [ConNF.Params] {τ : Type u} [Group τ] (α : ConNF.TypeIndex) : Group (ConNF.Tree τ α)

The group structure on the type of α-trees of τ is given by "branchwise" multiplication, given by Pi.group.

Equations

• ConNF.Tree.group α = Pi.group

@[simp]

theorem ConNF.Tree.one_apply [ConNF.Params] {τ : Type u} [Group τ] {α : ConNF.TypeIndex} (A : ConNF.ExtendedIndex α) : 1 A = 1

@[simp]

theorem ConNF.Tree.mul_apply [ConNF.Params] {τ : Type u} [Group τ] {α : ConNF.TypeIndex} (a : ConNF.Tree τ α) (a' : ConNF.Tree τ α) (A : ConNF.ExtendedIndex α) : (a * a') A = a A * a' A

@[simp]

theorem ConNF.Tree.inv_apply [ConNF.Params] {τ : Type u} [Group τ] {α : ConNF.TypeIndex} (a : ConNF.Tree τ α) (A : ConNF.ExtendedIndex α) : a⁻¹ A = (a A)⁻¹

def ConNF.Tree.toBotIso [ConNF.Params] {τ : Type u} [Group τ] : τ ≃* ConNF.Tree τ ⊥

The group isomorphism between τ and Tree ⊥ τ.

Equations

• ConNF.Tree.toBotIso = let __spread.0 := ConNF.Tree.toBot; { toEquiv := __spread.0, map_mul' := ⋯ }

@[simp]

theorem ConNF.Tree.coe_toBotIso [ConNF.Params] {τ : Type u} [Group τ] : ⇑ConNF.Tree.toBotIso = ⇑ConNF.Tree.toBot

@[simp]

theorem ConNF.Tree.coe_toBotIso_symm [ConNF.Params] {τ : Type u} [Group τ] : ⇑ConNF.Tree.toBotIso.symm = ⇑ConNF.Tree.ofBot

@[simp]

theorem ConNF.Tree.toBot_one [ConNF.Params] {τ : Type u} [Group τ] : ConNF.Tree.toBot 1 = 1

@[simp]

theorem ConNF.Tree.ofBot_one [ConNF.Params] {τ : Type u} [Group τ] : ConNF.Tree.ofBot 1 = 1

@[simp]

theorem ConNF.Tree.toBot_mul [ConNF.Params] {τ : Type u} [Group τ] (a : τ) (a' : τ) : ConNF.Tree.toBot (a * a') = ConNF.Tree.toBot a * ConNF.Tree.toBot a'

@[simp]

theorem ConNF.Tree.ofBot_mul [ConNF.Params] {τ : Type u} [Group τ] (a : ConNF.Tree τ ⊥) (a' : ConNF.Tree τ ⊥) : ConNF.Tree.ofBot (a * a') = ConNF.Tree.ofBot a * ConNF.Tree.ofBot a'

@[simp]

theorem ConNF.Tree.toBot_inv [ConNF.Params] {τ : Type u} [Group τ] (a : τ) : ConNF.Tree.toBot a⁻¹ = (ConNF.Tree.toBot a)⁻¹

@[simp]

theorem ConNF.Tree.ofBot_inv [ConNF.Params] {τ : Type u} [Group τ] (a : ConNF.Tree τ ⊥) : ConNF.Tree.ofBot a⁻¹ = (ConNF.Tree.ofBot a)⁻¹

@[simp]

theorem Quiver.Hom.comp_toPath {V : Type u_1} [Quiver V] {a : V} {b : V} {c : V} {p : Quiver.Path a b} {e : b ⟶ c} : p.comp e.toPath = p.cons e

@[simp]

theorem Quiver.Hom.comp_toPath_comp {V : Type u_1} [Quiver V] {a : V} {b : V} {c : V} {d : V} {p : Quiver.Path a b} {e : b ⟶ c} {q : Quiver.Path c d} : p.comp (e.toPath.comp q) = (p.cons e).comp q

def ConNF.Tree.comp [ConNF.Params] {τ : Type u} {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (A : Quiver.Path α β) (a : ConNF.Tree τ α) : ConNF.Tree τ β

The derivative functor. For a path from α to β, this is a map from α-trees of τ to β-trees of τ.

This is a functor from the category of type indices where the morphisms are the decreasing paths (i.e. the category where morphisms are elements of Path α β for α, β : TypeIndex) to the category of all trees of a fixed type τ, where the morphisms are functions.

If τ has a group structure, this map preserves multiplication. This means that we can treat this as a functor to the category of all trees on τ where the morphisms are group homomorphisms.

Equations

• ConNF.Tree.comp A a B = a (A.comp B)

theorem ConNF.Tree.comp_def [ConNF.Params] {τ : Type u} {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (A : Quiver.Path α β) (a : ConNF.Tree τ α) : ConNF.Tree.comp A a = fun (B : Quiver.Path β ⊥) => a (A.comp B)

@[simp]

theorem ConNF.Tree.comp_apply [ConNF.Params] {τ : Type u} {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (a : ConNF.Tree τ α) (A : Quiver.Path α β) (B : ConNF.ExtendedIndex β) : ConNF.Tree.comp A a B = a (A.comp B)

Evaluating the derivative of a structural group element along a path is the same as evaluating the original element along the composition of the paths.

@[simp]

theorem ConNF.Tree.comp_nil [ConNF.Params] {τ : Type u} {α : ConNF.TypeIndex} (a : ConNF.Tree τ α) : ConNF.Tree.comp Quiver.Path.nil a = a

The derivative along the empty path does nothing.

theorem ConNF.Tree.comp_cons [ConNF.Params] {τ : Type u} {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (a : ConNF.Tree τ α) (p : Quiver.Path α β) {γ : ConNF.TypeIndex} (h : γ < β) : ConNF.Tree.comp (p.cons h) a = ConNF.Tree.comp (Quiver.Hom.toPath h) (ConNF.Tree.comp p a)

theorem ConNF.Tree.comp_comp [ConNF.Params] {τ : Type u} {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} (a : ConNF.Tree τ α) (p : Quiver.Path α β) (q : Quiver.Path β γ) : ConNF.Tree.comp q (ConNF.Tree.comp p a) = ConNF.Tree.comp (p.comp q) a

The derivative map is functorial.

@[simp]

theorem ConNF.Tree.comp_one [ConNF.Params] {τ : Type u} [Group τ] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (A : Quiver.Path α β) : ConNF.Tree.comp A 1 = 1

The derivative map preserves the identity.

theorem ConNF.Tree.comp_mul [ConNF.Params] {τ : Type u} [Group τ] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (a₁ : ConNF.Tree τ α) (a₂ : ConNF.Tree τ α) (A : Quiver.Path α β) : ConNF.Tree.comp A (a₁ * a₂) = ConNF.Tree.comp A a₁ * ConNF.Tree.comp A a₂

The derivative map preserves multiplication.

theorem ConNF.Tree.comp_inv [ConNF.Params] {τ : Type u} [Group τ] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (a : ConNF.Tree τ α) (A : Quiver.Path α β) : (ConNF.Tree.comp A a)⁻¹ = ConNF.Tree.comp A a⁻¹

The derivative map preserves inverses.

@[simp]

theorem ConNF.Tree.comp_bot [ConNF.Params] {τ : Type u} {α : ConNF.TypeIndex} (a : ConNF.Tree τ α) (A : Quiver.Path α ⊥) : ConNF.Tree.comp A a = ConNF.Tree.toBot (a A)

instance ConNF.Tree.instMulActionBotTypeIndex [ConNF.Params] {τ : Type u} [Group τ] {X : Type u_1} [MulAction τ X] : MulAction (ConNF.Tree τ ⊥) X

⊥-trees on τ can act on everything that τ can.

Equations

• ConNF.Tree.instMulActionBotTypeIndex = MulAction.compHom X ConNF.Tree.toBotIso.symm.toMonoidHom

@[simp]

theorem ConNF.Tree.toBot_smul [ConNF.Params] {τ : Type u} [Group τ] {X : Type u_1} [MulAction τ X] (a : τ) (x : X) : ConNF.Tree.toBot a • x = a • x

@[simp]

theorem ConNF.Tree.ofBot_smul [ConNF.Params] {τ : Type u} [Group τ] {X : Type u_1} [MulAction τ X] (a : ConNF.Tree τ ⊥) (x : X) : ConNF.Tree.ofBot a • x = a • x

@[simp]

theorem ConNF.Tree.toBot_inv_smul [ConNF.Params] {τ : Type u} [Group τ] {X : Type u_1} [MulAction τ X] (a : τ) (x : X) : (ConNF.Tree.toBot a)⁻¹ • x = a⁻¹ • x

@[simp]

theorem ConNF.Tree.ofBot_inv_smul [ConNF.Params] {τ : Type u} [Group τ] {X : Type u_1} [MulAction τ X] (a : ConNF.Tree τ ⊥) (x : X) : (ConNF.Tree.ofBot a)⁻¹ • x = a⁻¹ • x