Structural actions

In this file, we define structural actions, and prove the freedom of action theorem for actions.

Main declarations

• ConNF.StrAction: Structural actions.

@[reducible, inline]

abbrev ConNF.StrAction [Params] : TypeIndex → Type u

Equations

• ConNF.StrAction = ConNF.Tree ConNF.BaseAction

def ConNF.StrAction.Coherent [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : StrAction β) : Prop

Equations

• ξ.Coherent = ∀ (A : β ↝ ⊥) (L₁ L₂ : ConNF.Litter), (ξ A)ᴸ L₁ L₂ → ConNF.CoherentAt ξ A L₁ L₂

theorem ConNF.StrAction.Coherent.deriv [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ξ : StrAction β} (hξ : ξ.Coherent) {γ : TypeIndex} [LeLevel γ] (A : β ↝ γ) : Coherent (ξ ⇘ A)

theorem ConNF.StrAction.mapFlexible_of_coherent [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ξ : StrAction β} (hξ : ξ.Coherent) (A : β ↝ ⊥) : (ξ A).MapFlexible A

structure ConNF.BaseAction.Approximates [Params] (ξ : BaseAction) (π : BasePerm) : Prop

TODO: Maybe move this to BaseActionClass?

• atoms (a₁ a₂ : Atom) : ξᴬ a₁ a₂ → a₂ = π • a₁
• nearLitters (N₁ N₂ : NearLitter) : ξᴺ N₁ N₂ → N₂ = π • N₁

theorem ConNF.BaseAction.Approximates.litters [Params] {ξ : BaseAction} {π : BasePerm} (h : ξ.Approximates π) (L₁ L₂ : Litter) : ξᴸ L₁ L₂ → π • L₁ = L₂

theorem ConNF.BaseAction.Approximates.mono [Params] {ψ χ : BaseAction} {π : BasePerm} (hχ : χ.Approximates π) (h : ψ ≤ χ) : ψ.Approximates π

def ConNF.StrAction.Approximates [Params] {β : TypeIndex} [ModelData β] (ξ : StrAction β) (ρ : AllPerm β) : Prop

Equations

• ξ.Approximates ρ = ∀ (A : β ↝ ⊥), (ξ A).Approximates (ρᵁ A)

def ConNF.StrAction.flexApprox [Params] [Level] {β : TypeIndex} [LeLevel β] [CoherentData] (ξ : StrAction β) : StrApprox β

Equations

• ξ.flexApprox A = (ξ A).flexApprox A

theorem ConNF.StrAction.flexApprox_coherent [Params] [Level] {β : TypeIndex} [LeLevel β] [CoherentData] (ξ : StrAction β) (hξ : ∀ (A : β ↝ ⊥), (ξ A).MapFlexible A) : ξ.flexApprox.Coherent

TODO: Put this in the blueprint.