Completing permutations

Litter actions can be turned into approximations by completing orbits of atoms and litters. In this file, we describe a procedure for doing this process. The base approximation that we compute will only remember images of A-flexible litters for some fixed A, for use in the freedom of action theorem.

Main declarations

• ConNF.BaseLAction.complete: A base approximation computed from a given base litter action.
• ConNF.BaseLAction.smul_nearLitter_eq_of_preciseAt: If ψ is a precise litter action that is completed to form φ, and φ exactly approximates π, then precise images of near-litters under ψ and π agree, so long as their rough images agree. The condition about rough images is required since the completion operation forgets all but the flexible litters.

noncomputable def ConNF.BaseLAction.sandboxLitter [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.Litter

The sandbox litter for a base litter action is an arbitrarily chosen litter that isn't banned.

Equations

• φ.sandboxLitter = ↑⋯.some

theorem ConNF.BaseLAction.sandboxLitter_not_banned [ConNF.Params] (φ : ConNF.BaseLAction) : ¬φ.BannedLitter φ.sandboxLitter

theorem ConNF.BaseLAction.mk_atomMap_image_le_mk_sandbox [ConNF.Params] (φ : ConNF.BaseLAction) : Cardinal.mk ↑(symmDiff φ.atomMap.Dom (φ.atomMapOrElse '' φ.atomMap.Dom)) ≤ Cardinal.mk ↑(ConNF.litterSet φ.sandboxLitter)

theorem ConNF.BaseLAction.disjoint_sandbox [ConNF.Params] (φ : ConNF.BaseLAction) : Disjoint (φ.atomMap.Dom ∪ φ.atomMapOrElse '' φ.atomMap.Dom) (ConNF.litterSet φ.sandboxLitter)

noncomputable def ConNF.BaseLAction.atomPartialPerm [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) : PartialPerm ConNF.Atom

A local permutation induced by completing the orbits of atoms in a base litter action. This function creates forward and backward images of atoms in the sandbox litter, a litter which is away from the domain and range of the approximation in question, so it should not interfere with other constructions.

Equations

• φ.atomPartialPerm hφ = PartialPerm.complete φ.atomMapOrElse φ.atomMap.Dom (ConNF.litterSet φ.sandboxLitter) ⋯ ⋯ ⋯ ⋯

theorem ConNF.BaseLAction.sandboxSubset_small [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.Small (PartialPerm.sandboxSubset ⋯ ⋯)

theorem ConNF.BaseLAction.atomPartialPerm_domain_small [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) : ConNF.Small (φ.atomPartialPerm hφ).domain

noncomputable def ConNF.BaseLAction.complete [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (hφ : φ.Lawful) (A : ConNF.ExtendedIndex ↑β) : ConNF.BaseApprox

A near-litter approximation built from this base litter action. Its action on atoms matches that of the action, and its rough action on flexible litters matches the given litter permutation.

Equations

• φ.complete hφ A = { atomPerm := φ.atomPartialPerm hφ, litterPerm := φ.flexibleLitterPartialPerm hφ A, domain_small := ⋯ }

theorem ConNF.BaseLAction.atomPartialPerm_apply_eq [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {a : ConNF.Atom} (ha : (φ.atomMap a).Dom) : (φ.atomPartialPerm hφ).toFun a = (φ.atomMap a).get ha

theorem ConNF.BaseLAction.complete_smul_atom_eq [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {hφ : φ.Lawful} {a : ConNF.Atom} (ha : (φ.atomMap a).Dom) : φ.complete hφ A • a = (φ.atomMap a).get ha

@[simp]

theorem ConNF.BaseLAction.complete_smul_litter_eq [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {hφ : φ.Lawful} (L : ConNF.Litter) : φ.complete hφ A • L = (φ.flexibleLitterPartialPerm hφ A).toFun L

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

theorem ConNF.BaseLAction.smul_toNearLitter_eq_of_preciseAt [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {hφ : φ.Lawful} {π : ConNF.BasePerm} (hπ : (φ.complete hφ A).ExactlyApproximates π) {L : ConNF.Litter} (hL : (φ.litterMap L).Dom) (hφL : φ.PreciseAt hL) (hπL : π • L = ((φ.litterMap L).get hL).fst) : π • L.toNearLitter = (φ.litterMap L).get hL

theorem ConNF.BaseLAction.smul_nearLitter_eq_of_preciseAt [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {hφ : φ.Lawful} {π : ConNF.BasePerm} (hπ : (φ.complete hφ A).ExactlyApproximates π) {N : ConNF.NearLitter} (hN : (φ.litterMap N.fst).Dom) (hw : φ.PreciseAt hN) (hπL : π • N.fst = ((φ.litterMap N.fst).get hN).fst) : ↑(π • N) = symmDiff (↑((φ.litterMap N.fst).get hN)) (π • symmDiff (ConNF.litterSet N.fst) ↑N)