Documentation

ConNF.FOA.StrAction

Structural actions #

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

Main declarations #

source
@[reducible, inline]
abbrev ConNF.StrAction [ConNF.Params] :
ConNF.TypeIndex → Type u
Equations
Instances For
    source
    def ConNF.StrAction.Coherent [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ξ : ConNF.StrAction β) :
    Prop
    Equations
    Instances For
      source
      theorem ConNF.StrAction.Coherent.deriv [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ξ : ConNF.StrAction β} (hξ : ξ.Coherent) {γ : ConNF.TypeIndex} [ConNF.LeLevel γ] (A : β ↝ γ) :
      ConNF.StrAction.Coherent (ξ ⇘ A)
      source
      theorem ConNF.StrAction.mapFlexible_of_coherent [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ξ : ConNF.StrAction β} (hξ : ξ.Coherent) (A : β ↝ ⊥) :
      (ξ A).MapFlexible A
      source
      structure ConNF.BaseAction.Approximates [ConNF.Params] (ξ : ConNF.BaseAction) (π : ConNF.BasePerm) :
      Prop

      TODO: Maybe move this to BaseActionClass?

      • atoms : ∀ (a₁ a₂ : ConNF.Atom), ξᴬ a₁ a₂ → a₂ = π • a₁
      • nearLitters : ∀ (N₁ N₂ : ConNF.NearLitter), ξᴺ N₁ N₂ → N₂ = π • N₁
      Instances For
        source
        theorem ConNF.BaseAction.Approximates.litters [ConNF.Params] {ξ : ConNF.BaseAction} {π : ConNF.BasePerm} (h : ξ.Approximates π) (L₁ L₂ : ConNF.Litter) :
        ξᴸ L₁ L₂ → π • L₁ = L₂
        source
        theorem ConNF.BaseAction.Approximates.mono [ConNF.Params] {ψ χ : ConNF.BaseAction} {π : ConNF.BasePerm} (hχ : χ.Approximates π) (h : ψ ≤ χ) :
        ψ.Approximates π
        source
        def ConNF.StrAction.Approximates [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.ModelData β] (ξ : ConNF.StrAction β) (ρ : ConNF.AllPerm β) :
        Prop
        Equations
        • ξ.Approximates ρ = ∀ (A : β ↝ ⊥), (ξ A).Approximates (ρᵁ A)
        Instances For
          source
          def ConNF.StrAction.flexApprox [ConNF.Params] [ConNF.Level] {β : ConNF.TypeIndex} [ConNF.LeLevel β] [ConNF.CoherentData] (ξ : ConNF.StrAction β) :
          ConNF.StrApprox β
          Equations
          • ξ.flexApprox A = (ξ A).flexApprox A
          Instances For
            source
            theorem ConNF.StrAction.flexApprox_coherent [ConNF.Params] [ConNF.Level] {β : ConNF.TypeIndex} [ConNF.LeLevel β] [ConNF.CoherentData] (ξ : ConNF.StrAction β) (hξ : ∀ (A : β ↝ ⊥), (ξ A).MapFlexible A) :
            ξ.flexApprox.Coherent

            TODO: Put this in the blueprint.