Structural litter actions

In this file, we define structural litter actions, which are trees of base litter actions.

Main declarations

• ConNF.StructLAction: A tree of base litter actions.
• ConNF.StructLAction.Lawful, ConNF.StructLAction.Approximates: Branchwise definitions of lawfulness and approximation.
• ConNF.StructLAction.complete: A structural approximation given by completing orbits branchwise.

@[reducible, inline]

abbrev ConNF.StructLAction [ConNF.Params] (α : ConNF.TypeIndex) : Type u

A β-structural action is a β-tree of base litter actions.

Equations

• ConNF.StructLAction = ConNF.Tree ConNF.BaseLAction

def ConNF.StructLAction.Lawful [ConNF.Params] {β : ConNF.TypeIndex} (φ : ConNF.StructLAction β) : Prop

Equations

• φ.Lawful = ∀ (B : ConNF.ExtendedIndex β), (φ B).Lawful

def ConNF.StructLAction.Approximates [ConNF.Params] {β : ConNF.TypeIndex} (ψ : ConNF.StructLAction β) (π : ConNF.StructPerm β) : Prop

Equations

• ψ.Approximates π = ∀ (A : ConNF.ExtendedIndex β), (ψ A).Approximates (π A)

def ConNF.StructLAction.MapFlexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (φ : ConNF.StructLAction ↑β) : Prop

This structural action maps flexible litters to flexible litters.

Equations

• φ.MapFlexible = ∀ (B : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (hL : ((φ B).litterMap L).Dom), ConNF.Flexible B L → ConNF.Flexible B (((φ B).litterMap L).get hL).fst

def ConNF.StructLAction.Precise [ConNF.Params] {β : ConNF.TypeIndex} (φ : ConNF.StructLAction β) : Prop

Equations

• φ.Precise = ∀ (B : ConNF.ExtendedIndex β), (φ B).Precise

noncomputable def ConNF.StructLAction.complete [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (φ : ConNF.StructLAction ↑β) (hφ : φ.Lawful) : ConNF.StructApprox ↑β

Equations

• φ.complete hφ B = (φ B).complete ⋯ B

theorem ConNF.StructLAction.complete_apply [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (φ : ConNF.StructLAction ↑β) (hφ : φ.Lawful) (B : ConNF.ExtendedIndex ↑β) : φ.complete hφ B = (φ B).complete ⋯ B

theorem ConNF.StructLAction.smul_atom_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (φ : ConNF.StructLAction ↑β) {hφ : φ.Lawful} {π : ConNF.StructPerm ↑β} (hπ : (φ.complete hφ).ExactlyApproximates π) {a : ConNF.Atom} {B : ConNF.ExtendedIndex ↑β} (ha : ((φ B).atomMap a).Dom) : π B • a = ((φ B).atomMap a).get ha

theorem ConNF.StructLAction.smul_toNearLitter_eq_of_precise [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (φ : ConNF.StructLAction ↑β) {hφ : φ.Lawful} (hφp : φ.Precise) {π : ConNF.StructPerm ↑β} (hπ : (φ.complete hφ).ExactlyApproximates π) {L : ConNF.Litter} {B : ConNF.ExtendedIndex ↑β} (hL : ((φ B).litterMap L).Dom) (hπL : π B • L = (((φ B).litterMap L).get hL).fst) : π B • L.toNearLitter = ((φ B).litterMap L).get hL

theorem ConNF.StructLAction.smul_nearLitter_eq_of_precise [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (φ : ConNF.StructLAction ↑β) {hφ : φ.Lawful} (hφp : φ.Precise) {π : ConNF.StructPerm ↑β} (hπ : (φ.complete hφ).ExactlyApproximates π) {N : ConNF.NearLitter} {B : ConNF.ExtendedIndex ↑β} (hN : ((φ B).litterMap N.fst).Dom) (hπL : π B • N.fst = (((φ B).litterMap N.fst).get hN).fst) : ↑(π B • N) = symmDiff (↑(((φ B).litterMap N.fst).get hN)) (ConNF.Tree.comp B π • symmDiff (ConNF.litterSet N.fst) ↑N)

instance ConNF.StructLAction.instPartialOrder [ConNF.Params] {β : ConNF.TypeIndex} : PartialOrder (ConNF.StructLAction β)

Equations

• ConNF.StructLAction.instPartialOrder = PartialOrder.mk ⋯

theorem ConNF.StructLAction.Lawful.le [ConNF.Params] {β : ConNF.TypeIndex} {φ : ConNF.StructLAction β} {ψ : ConNF.StructLAction β} (h : φ.Lawful) (hψ : ψ ≤ φ) : ψ.Lawful

theorem ConNF.StructLAction.le_comp [ConNF.Params] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} {φ : ConNF.StructLAction β} {ψ : ConNF.StructLAction β} (h : φ ≤ ψ) (A : Quiver.Path β γ) : ConNF.Tree.comp A φ ≤ ConNF.Tree.comp A ψ

theorem ConNF.StructLAction.Lawful.comp [ConNF.Params] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} {φ : ConNF.StructLAction β} (h : φ.Lawful) (A : Quiver.Path β γ) : ConNF.StructLAction.Lawful (ConNF.Tree.comp A φ)