Converting actions into approximations

In this file, we combine the processes defined in ConNF.FOA.LAction.FillAtomOrbits, ConNF.FOA.LAction.FillAtomRange, and ConNF.FOA.LAction.Complete, which allows us to turn arbitrary litter actions into approximations.

Main declarations

• ConNF.BaseLAction.toApprox: Converts a base litter action ψ into a base approximation φ in such a way that if φ exactly approximates π, then

  1. ψ agrees with π on all atoms and flexible litters; and
  2. for any near-litter N, if ψ agrees with π on N.1, then ψ agrees with π on N.

noncomputable def ConNF.BaseLAction.refine [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) : ConNF.BaseLAction

Equations

• φ.refine hφ = φ.fillAtomRange.fillAtomOrbits ⋯

theorem ConNF.BaseLAction.refineLawful [ConNF.Params] {φ : ConNF.BaseLAction} {hφ : φ.Lawful} : (φ.refine hφ).Lawful

@[simp]

theorem ConNF.BaseLAction.refine_atomMap [ConNF.Params] {φ : ConNF.BaseLAction} {hφ : φ.Lawful} {a : ConNF.Atom} (ha : (φ.atomMap a).Dom) : (φ.refine hφ).atomMap a = φ.atomMap a

@[simp]

theorem ConNF.BaseLAction.refine_atomMap_get [ConNF.Params] {φ : ConNF.BaseLAction} {hφ : φ.Lawful} {a : ConNF.Atom} (ha : (φ.atomMap a).Dom) : ((φ.refine hφ).atomMap a).get ⋯ = (φ.atomMap a).get ha

@[simp]

theorem ConNF.BaseLAction.refine_litterMap [ConNF.Params] {φ : ConNF.BaseLAction} {hφ : φ.Lawful} : (φ.refine hφ).litterMap = φ.litterMap

theorem ConNF.BaseLAction.refine_precise [ConNF.Params] {φ : ConNF.BaseLAction} {hφ : φ.Lawful} : (φ.refine hφ).Precise

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

Equations

• φ.refine hφ A = (φ A).refine ⋯

theorem ConNF.StructLAction.refine_lawful [ConNF.Params] {β : ConNF.TypeIndex} {φ : ConNF.StructLAction β} {hφ : φ.Lawful} : (φ.refine hφ).Lawful

@[simp]

theorem ConNF.StructLAction.refine_apply [ConNF.Params] {β : ConNF.TypeIndex} {φ : ConNF.StructLAction β} {hφ : φ.Lawful} {A : ConNF.ExtendedIndex β} : φ.refine hφ A = (φ A).refine ⋯

theorem ConNF.StructLAction.refine_atomMap [ConNF.Params] {β : ConNF.TypeIndex} {φ : ConNF.StructLAction β} {hφ : φ.Lawful} {A : ConNF.ExtendedIndex β} {a : ConNF.Atom} (ha : ((φ A).atomMap a).Dom) : ((φ A).refine ⋯).atomMap a = (φ A).atomMap a

@[simp]

theorem ConNF.StructLAction.refine_atomMap_get [ConNF.Params] {β : ConNF.TypeIndex} {φ : ConNF.StructLAction β} {hφ : φ.Lawful} {A : ConNF.ExtendedIndex β} {a : ConNF.Atom} (ha : ((φ A).atomMap a).Dom) : (((φ A).refine ⋯).atomMap a).get ⋯ = ((φ A).atomMap a).get ha

@[simp]

theorem ConNF.StructLAction.refine_litterMap [ConNF.Params] {β : ConNF.TypeIndex} {φ : ConNF.StructLAction β} {hφ : φ.Lawful} {A : ConNF.ExtendedIndex β} : ((φ A).refine ⋯).litterMap = (φ A).litterMap

theorem ConNF.StructLAction.refine_precise [ConNF.Params] {β : ConNF.TypeIndex} {φ : ConNF.StructLAction β} {hφ : φ.Lawful} : (φ.refine hφ).Precise

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

Refine and complete this action into a structural approximation.

Equations

• φ.toApprox h = (φ.refine h).complete ⋯

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

theorem ConNF.StructLAction.toApprox_smul_litter_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {φ : ConNF.StructLAction ↑β} {hφ : φ.Lawful} {B : ConNF.ExtendedIndex ↑β} (L : ConNF.Litter) : φ.toApprox hφ B • L = ((φ.refine hφ B).flexibleLitterPartialPerm ⋯ B).toFun L

theorem ConNF.StructLAction.toApprox_symm_smul_litter_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {φ : ConNF.StructLAction ↑β} {hφ : φ.Lawful} {B : ConNF.ExtendedIndex ↑β} (L : ConNF.Litter) : (φ.toApprox hφ B).symm • L = ((φ.refine hφ B).flexibleLitterPartialPerm ⋯ B).symm.toFun L

theorem ConNF.StructLAction.toApprox_free [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (φ : ConNF.StructLAction ↑β) (h₁ : φ.Lawful) (h₂ : φ.MapFlexible) : (φ.toApprox h₁).Free

theorem ConNF.StructLAction.toApprox_comp_atomPerm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} {φ : ConNF.StructLAction ↑β} {hφ : φ.Lawful} (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A φ) ⋯ B).atomPerm = (φ.toApprox hφ (A.comp B)).atomPerm

theorem ConNF.StructLAction.toApprox_comp_smul_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} {φ : ConNF.StructLAction ↑β} {hφ : φ.Lawful} (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) (a : ConNF.Atom) : ConNF.StructLAction.toApprox (ConNF.Tree.comp A φ) ⋯ B • a = φ.toApprox hφ (A.comp B) • a