Documentation

ConNF.FOA.LAction.FillAtomOrbits

Filling in orbits of atoms #

In ConNF.FOA.LAction.Complete, we showed how precise litter actions can be turned into approximations with suitable properties. In this file, we show a process that allows us to turn certain actions into precise actions, by filling in orbits of atoms that interact with litters in exceptional ways. We later extend this to all actions in ConNF.FOA.LAction.FillAtomRange.

Main declarations #

ConNF.BaseLAction.fillAtomOrbits: Fills in orbits of certain atoms that behave exceptionally, but does not alter the litter map.
ConNF.BaseLAction.fillAtomOrbits_precise: Assuming a certain hypothesis on the range of ψ, the action we obtain from the fillAtomOrbits procedure is precise.

theorem ConNF.BaseLAction.mk_dom_symmDiff_le [ConNF.Params] (φ : ConNF.BaseLAction) :

Cardinal.mk ↑(symmDiff φ.litterMap.Dom (φ.roughLitterMapOrElse '' φ.litterMap.Dom)) ≤ Cardinal.mk ↑{L : ConNF.Litter | ¬φ.BannedLitter L}

theorem ConNF.BaseLAction.aleph0_le_not_bannedLitter [ConNF.Params] (φ : ConNF.BaseLAction) :

Cardinal.aleph0 ≤ Cardinal.mk ↑{L : ConNF.Litter | ¬φ.BannedLitter L}

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

PartialPerm ConNF.Litter

A local permutation on the set of litters that occur in the domain or range of w. This permutes both flexible and inflexible litters. This is only used to control orbits of atoms, and will not be used for the litter permutation in a base approximation.

Equations

φ.litterPerm' hφ = PartialPerm.complete φ.roughLitterMapOrElse φ.litterMap.Dom {L : ConNF.Litter | ¬φ.BannedLitter L} ⋯ ⋯ ⋯ ⋯

Instances For

def ConNF.BaseLAction.idOnBanned [ConNF.Params] (φ : ConNF.BaseLAction) (s : Set ConNF.Litter) :

PartialPerm ConNF.Litter

Equations

φ.idOnBanned s = { toFun := id, invFun := id, domain := {L : ConNF.Litter | φ.BannedLitter L} \ s, toFun_domain' := ⋯, invFun_domain' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }

Instances For

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

PartialPerm ConNF.Litter

Equations

φ.litterPerm hφ = (φ.litterPerm' hφ).piecewise (φ.idOnBanned (φ.litterPerm' hφ).domain) ⋯

Instances For

theorem ConNF.BaseLAction.litterPerm'_apply_eq [ConNF.Params] {φ : ConNF.BaseLAction} {hφ : φ.Lawful} (L : ConNF.Litter) (hL : L ∈ φ.litterMap.Dom) :

(φ.litterPerm' hφ).toFun L = φ.roughLitterMapOrElse L

theorem ConNF.BaseLAction.litterPerm_apply_eq [ConNF.Params] {φ : ConNF.BaseLAction} {hφ : φ.Lawful} (L : ConNF.Litter) (hL : L ∈ φ.litterMap.Dom) :

(φ.litterPerm hφ).toFun L = φ.roughLitterMapOrElse L

theorem ConNF.BaseLAction.litterPerm'_domain_small [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) :

ConNF.Small (φ.litterPerm' hφ).domain

theorem ConNF.BaseLAction.litterPerm_domain_small [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) :

ConNF.Small (φ.litterPerm hφ).domain

def ConNF.BaseLAction.needForwardImages [ConNF.Params] (φ : ConNF.BaseLAction) :

Set ConNF.Atom

Equations

φ.needForwardImages = φ.atomMap.ran \ φ.atomMap.Dom

Instances For

def ConNF.BaseLAction.needBackwardImages [ConNF.Params] (φ : ConNF.BaseLAction) :

Set ConNF.Atom

Equations

φ.needBackwardImages = φ.atomMap.Dom \ φ.atomMap.ran

Instances For

theorem ConNF.BaseLAction.atomMap_ran_small [ConNF.Params] (φ : ConNF.BaseLAction) :

ConNF.Small φ.atomMap.ran

theorem ConNF.BaseLAction.needForwardImages_small [ConNF.Params] (φ : ConNF.BaseLAction) :

ConNF.Small φ.needForwardImages

theorem ConNF.BaseLAction.needBackwardImages_small [ConNF.Params] (φ : ConNF.BaseLAction) :

ConNF.Small φ.needBackwardImages

theorem ConNF.BaseLAction.mk_diff_dom_ran [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) :

Cardinal.mk ↑(ConNF.litterSet L \ (φ.atomMap.Dom ∪ φ.atomMap.ran)) = Cardinal.mk ConNF.κ

theorem ConNF.BaseLAction.need_images_small [ConNF.Params] (φ : ConNF.BaseLAction) :

Cardinal.mk (ℕ × ↑φ.needBackwardImages ⊕ ℕ × ↑φ.needForwardImages) < Cardinal.mk ConNF.κ

theorem ConNF.BaseLAction.le_mk_diff_dom_ran [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) :

Cardinal.mk (ℕ × ↑φ.needBackwardImages ⊕ ℕ × ↑φ.needForwardImages) ≤ Cardinal.mk ↑(ConNF.litterSet L \ (φ.atomMap.Dom ∪ φ.atomMap.ran))

def ConNF.BaseLAction.orbitSet [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) :

Set ConNF.Atom

Equations

φ.orbitSet L = ⋯.choose

Instances For

theorem ConNF.BaseLAction.orbitSet_subset [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) :

φ.orbitSet L ⊆ ConNF.litterSet L \ (φ.atomMap.Dom ∪ φ.atomMap.ran)

theorem ConNF.BaseLAction.not_mem_needForwardImages_of_mem_orbitSet [ConNF.Params] (φ : ConNF.BaseLAction) {a : ConNF.Atom} {L : ConNF.Litter} (h : a ∈ φ.orbitSet L) :

a ∉ φ.needForwardImages

theorem ConNF.BaseLAction.not_mem_needBackwardImages_of_mem_orbitSet [ConNF.Params] (φ : ConNF.BaseLAction) {a : ConNF.Atom} {L : ConNF.Litter} (h : a ∈ φ.orbitSet L) :

a ∉ φ.needBackwardImages

theorem ConNF.BaseLAction.mk_orbitSet [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) :

Cardinal.mk ↑(φ.orbitSet L) = Cardinal.mk (ℕ × ↑φ.needBackwardImages ⊕ ℕ × ↑φ.needForwardImages)

@[irreducible]

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

↑(φ.orbitSet L) ≃ ℕ × ↑φ.needBackwardImages ⊕ ℕ × ↑φ.needForwardImages

Equations

@ConNF.BaseLAction.orbitSetEquiv = ConNF.BaseLAction.wrapped✝.1

Instances For

theorem ConNF.BaseLAction.orbitSetEquiv_def [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) :

φ.orbitSetEquiv L = ⋯.some

theorem ConNF.BaseLAction.orbitSetEquiv_injective [ConNF.Params] (φ : ConNF.BaseLAction) {a₁ : ℕ × ↑φ.needBackwardImages ⊕ ℕ × ↑φ.needForwardImages} {a₂ : ℕ × ↑φ.needBackwardImages ⊕ ℕ × ↑φ.needForwardImages} {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} (h : ↑((φ.orbitSetEquiv L₁).symm a₁) = ↑((φ.orbitSetEquiv L₂).symm a₂)) :

L₁ = L₂ ∧ a₁ = a₂

theorem ConNF.BaseLAction.orbitSetEquiv_congr [ConNF.Params] (φ : ConNF.BaseLAction) {L : ConNF.Litter} {L' : ConNF.Litter} {a : ConNF.Atom} (ha : a ∈ φ.orbitSet L) (h : L = L') :

(φ.orbitSetEquiv L) ⟨a, ha⟩ = (φ.orbitSetEquiv L') ⟨a, ⋯⟩

theorem ConNF.BaseLAction.orbitSetEquiv_symm_congr [ConNF.Params] (φ : ConNF.BaseLAction) {L : ConNF.Litter} {L' : ConNF.Litter} {a : ℕ × ↑φ.needBackwardImages ⊕ ℕ × ↑φ.needForwardImages} (h : L = L') :

↑((φ.orbitSetEquiv L).symm a) = ↑((φ.orbitSetEquiv L').symm a)

theorem ConNF.BaseLAction.orbitSet_small [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) :

ConNF.Small (φ.orbitSet L)

noncomputable def ConNF.BaseLAction.nextForwardImage [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (L : ConNF.Litter) (a : ℕ × ↑φ.needForwardImages) :

ConNF.Atom

Equations

φ.nextForwardImage hφ L a = ↑((φ.orbitSetEquiv ((φ.litterPerm hφ).toFun L)).symm (Sum.inr (a.1 + 1, a.2)))

Instances For

noncomputable def ConNF.BaseLAction.nextBackwardImage [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (L : ConNF.Litter) :

ℕ × ↑φ.needBackwardImages → ConNF.Atom

Equations

φ.nextBackwardImage hφ L x = match x with | (0, a) => ↑a | (n.succ, a) => ↑((φ.orbitSetEquiv ((φ.litterPerm hφ).toFun L)).symm (Sum.inl (n, a)))

Instances For

def ConNF.BaseLAction.nextForwardImageDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (L : ConNF.Litter) :

Set (ℕ × ↑φ.needForwardImages)

Equations

φ.nextForwardImageDomain hφ L = {a : ℕ × ↑φ.needForwardImages | (↑a.2).1 ∈ (φ.litterPerm hφ).domain ∧ (φ.litterPerm hφ).toFun^[a.1 + 1] (↑a.2).1 = L}

Instances For

def ConNF.BaseLAction.nextBackwardImageDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (L : ConNF.Litter) :

Set (ℕ × ↑φ.needBackwardImages)

Equations

φ.nextBackwardImageDomain hφ L = {a : ℕ × ↑φ.needBackwardImages | (↑a.2).1 ∈ (φ.litterPerm hφ).domain ∧ (φ.litterPerm hφ).symm.toFun^[a.1 + 1] (↑a.2).1 = L}

Instances For

theorem ConNF.BaseLAction.mk_mem_nextForwardImageDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (L : ConNF.Litter) (n : ℕ) (a : ↑φ.needForwardImages) :

(n, a) ∈ φ.nextForwardImageDomain hφ L ↔ (↑a).1 ∈ (φ.litterPerm hφ).domain ∧ (φ.litterPerm hφ).toFun^[n + 1] (↑a).1 = L

theorem ConNF.BaseLAction.mk_mem_nextBackwardImageDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (L : ConNF.Litter) (n : ℕ) (a : ↑φ.needBackwardImages) :

(n, a) ∈ φ.nextBackwardImageDomain hφ L ↔ (↑a).1 ∈ (φ.litterPerm hφ).domain ∧ (φ.litterPerm hφ).symm.toFun^[n + 1] (↑a).1 = L

theorem ConNF.BaseLAction.nextForwardImage_eq [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {a : ℕ × ↑φ.needForwardImages} {b : ℕ × ↑φ.needForwardImages} (hL₁ : L₁ ∈ (φ.litterPerm hφ).domain) (hL₂ : L₂ ∈ (φ.litterPerm hφ).domain) (h : φ.nextForwardImage hφ L₁ a = φ.nextForwardImage hφ L₂ b) :

L₁ = L₂

theorem ConNF.BaseLAction.nextBackwardImage_eq [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {a : ℕ × ↑φ.needBackwardImages} {b : ℕ × ↑φ.needBackwardImages} (ha : a ∈ φ.nextBackwardImageDomain hφ L₁) (hb : b ∈ φ.nextBackwardImageDomain hφ L₂) (hL₁ : L₁ ∈ (φ.litterPerm hφ).domain) (hL₂ : L₂ ∈ (φ.litterPerm hφ).domain) (h : φ.nextBackwardImage hφ L₁ a = φ.nextBackwardImage hφ L₂ b) :

L₁ = L₂

theorem ConNF.BaseLAction.nextForwardImage_injective [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {L : ConNF.Litter} {a : ℕ × ↑φ.needForwardImages} {b : ℕ × ↑φ.needForwardImages} (h : φ.nextForwardImage hφ L a = φ.nextForwardImage hφ L b) :

a = b

theorem ConNF.BaseLAction.nextBackwardImage_injective [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {L : ConNF.Litter} {a : ℕ × ↑φ.needBackwardImages} {b : ℕ × ↑φ.needBackwardImages} (ha : a ∈ φ.nextBackwardImageDomain hφ L) (hb : b ∈ φ.nextBackwardImageDomain hφ L) (h : φ.nextBackwardImage hφ L a = φ.nextBackwardImage hφ L b) :

a = b

theorem ConNF.BaseLAction.nextForwardImage_injective' [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {a : ℕ × ↑φ.needForwardImages} {b : ℕ × ↑φ.needForwardImages} (hL₁ : L₁ ∈ (φ.litterPerm hφ).domain) (hL₂ : L₂ ∈ (φ.litterPerm hφ).domain) (h : φ.nextForwardImage hφ L₁ a = φ.nextForwardImage hφ L₂ b) :

a = b

theorem ConNF.BaseLAction.nextBackwardImage_injective' [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {a : ℕ × ↑φ.needBackwardImages} {b : ℕ × ↑φ.needBackwardImages} (ha : a ∈ φ.nextBackwardImageDomain hφ L₁) (hb : b ∈ φ.nextBackwardImageDomain hφ L₂) (hL₁ : L₁ ∈ (φ.litterPerm hφ).domain) (hL₂ : L₂ ∈ (φ.litterPerm hφ).domain) (h : φ.nextBackwardImage hφ L₁ a = φ.nextBackwardImage hφ L₂ b) :

a = b

theorem ConNF.BaseLAction.nextForwardImage_ne_nextBackwardImage [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {a : ℕ × ↑φ.needForwardImages} {b : ℕ × ↑φ.needBackwardImages} :

φ.nextForwardImage hφ L₁ a ≠ φ.nextBackwardImage hφ L₂ b

noncomputable def ConNF.BaseLAction.nextImageCore [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (L : ConNF.Litter) (ha : a ∈ φ.orbitSet L) :

ConNF.Atom

Equations

φ.nextImageCore hφ a L ha = Sum.elim (φ.nextBackwardImage hφ L) (φ.nextForwardImage hφ L) ((φ.orbitSetEquiv L) ⟨a, ha⟩)

Instances For

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

Set ConNF.Atom

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem ConNF.BaseLAction.nextImageCoreDomain_small [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) :

ConNF.Small (φ.nextImageCoreDomain hφ)

theorem ConNF.BaseLAction.litter_map_dom_of_mem_nextImageCoreDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {a : ConNF.Atom} (h : a ∈ φ.nextImageCoreDomain hφ) :

a.1 ∈ (φ.litterPerm hφ).domain

theorem ConNF.BaseLAction.mem_orbitSet_of_mem_nextImageCoreDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {a : ConNF.Atom} (h : a ∈ φ.nextImageCoreDomain hφ) :

a ∈ φ.orbitSet a.1

theorem ConNF.BaseLAction.orbitSetEquiv_elim_of_mem_nextImageCoreDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) {a : ConNF.Atom} (h : a ∈ φ.nextImageCoreDomain hφ) :

Sum.elim (fun (x : ℕ × ↑φ.needBackwardImages) => x ∈ φ.nextBackwardImageDomain hφ a.1) (fun (x : ℕ × ↑φ.needForwardImages) => x ∈ φ.nextForwardImageDomain hφ a.1) ((φ.orbitSetEquiv a.1) ⟨a, ⋯⟩)

theorem ConNF.BaseLAction.nextImageCore_injective [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (b : ConNF.Atom) (ha : a ∈ φ.nextImageCoreDomain hφ) (hb : b ∈ φ.nextImageCoreDomain hφ) (h : φ.nextImageCore hφ a a.1 ⋯ = φ.nextImageCore hφ b b.1 ⋯) :

a = b

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

Set ConNF.Atom

Equations

φ.nextImageDomain hφ = φ.needForwardImages ∩ {a : ConNF.Atom | a.1 ∈ (φ.litterPerm hφ).domain} ∪ φ.nextImageCoreDomain hφ

Instances For

noncomputable def ConNF.BaseLAction.nextImage [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : a ∈ φ.nextImageDomain hφ) :

ConNF.Atom

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem ConNF.BaseLAction.nextImageDomain_small [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) :

ConNF.Small (φ.nextImageDomain hφ)

theorem ConNF.BaseLAction.disjoint_needForwardImages_nextImageCoreDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) :

Disjoint φ.needForwardImages (φ.nextImageCoreDomain hφ)

theorem ConNF.BaseLAction.nextImage_eq_of_needForwardImages [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : a ∈ φ.needForwardImages ∧ a.1 ∈ (φ.litterPerm hφ).domain) :

φ.nextImage hφ a ⋯ = ↑((φ.orbitSetEquiv ((φ.litterPerm hφ).toFun a.1)).symm (Sum.inr (0, ⟨a, ⋯⟩)))

theorem ConNF.BaseLAction.nextImage_eq_of_mem_nextImageCoreDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : a ∈ φ.nextImageCoreDomain hφ) :

φ.nextImage hφ a ⋯ = φ.nextImageCore hφ a a.1 ⋯

theorem ConNF.BaseLAction.orbitSetEquiv_ne_nextImageCore [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (b : ConNF.Atom) (ha : a ∈ φ.needForwardImages ∧ a.1 ∈ (φ.litterPerm hφ).domain) (hb : b ∈ φ.nextImageCoreDomain hφ) :

↑((φ.orbitSetEquiv ((φ.litterPerm hφ).toFun a.1)).symm (Sum.inr (0, ⟨a, ⋯⟩))) ≠ φ.nextImageCore hφ b b.1 ⋯

theorem ConNF.BaseLAction.nextImage_injective [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (b : ConNF.Atom) (ha : a ∈ φ.nextImageDomain hφ) (hb : b ∈ φ.nextImageDomain hφ) (h : φ.nextImage hφ a ha = φ.nextImage hφ b hb) :

a = b

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

ConNF.Atom →. ConNF.Atom

Equations

φ.orbitAtomMap hφ a = { Dom := (φ.atomMap a).Dom ∨ a ∈ φ.nextImageDomain hφ, get := fun (h : (φ.atomMap a).Dom ∨ a ∈ φ.nextImageDomain hφ) => h.elim' (φ.atomMap a).get (φ.nextImage hφ a) }

Instances For

@[simp]

theorem ConNF.BaseLAction.orbitAtomMap_dom_iff [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) :

(φ.orbitAtomMap hφ a).Dom ↔ (φ.atomMap a).Dom ∨ a ∈ φ.nextImageDomain hφ

@[simp]

theorem ConNF.BaseLAction.orbitAtomMap_dom [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) :

(φ.orbitAtomMap hφ).Dom = φ.atomMap.Dom ∪ φ.nextImageDomain hφ

theorem ConNF.BaseLAction.disjoint_atomMap_dom_nextImageDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) :

Disjoint φ.atomMap.Dom (φ.nextImageDomain hφ)

theorem ConNF.BaseLAction.orbitAtomMap_eq_of_mem_dom [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : (φ.atomMap a).Dom) :

(φ.orbitAtomMap hφ a).get ⋯ = (φ.atomMap a).get ha

theorem ConNF.BaseLAction.orbitAtomMap_eq_of_mem_nextImageDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : a ∈ φ.nextImageDomain hφ) :

(φ.orbitAtomMap hφ a).get ⋯ = φ.nextImage hφ a ha

theorem ConNF.BaseLAction.orbitAtomMap_eq_of_needForwardImages [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : a ∈ φ.needForwardImages ∧ a.1 ∈ (φ.litterPerm hφ).domain) :

(φ.orbitAtomMap hφ a).get ⋯ = ↑((φ.orbitSetEquiv ((φ.litterPerm hφ).toFun a.1)).symm (Sum.inr (0, ⟨a, ⋯⟩)))

theorem ConNF.BaseLAction.orbitAtomMap_eq_of_mem_nextImageCoreDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : a ∈ φ.nextImageCoreDomain hφ) :

(φ.orbitAtomMap hφ a).get ⋯ = φ.nextImageCore hφ a a.1 ⋯

theorem ConNF.BaseLAction.orbitAtomMap_dom_small [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) :

ConNF.Small (φ.orbitAtomMap hφ).Dom

theorem ConNF.BaseLAction.orbitAtomMap_apply_ne_of_needForwardImages [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) ⦃a : ConNF.Atom⦄ ⦃b : ConNF.Atom⦄ (ha : (φ.atomMap a).Dom) (hb : b ∈ φ.needForwardImages ∧ b.1 ∈ (φ.litterPerm hφ).domain) :

(φ.orbitAtomMap hφ a).get ⋯ ≠ (φ.orbitAtomMap hφ b).get ⋯

theorem ConNF.BaseLAction.orbitAtomMap_apply_ne_of_mem_nextImageCoreDomain [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) ⦃a : ConNF.Atom⦄ ⦃b : ConNF.Atom⦄ (ha : (φ.atomMap a).Dom) (hb : b ∈ φ.nextImageCoreDomain hφ) :

(φ.orbitAtomMap hφ a).get ⋯ ≠ (φ.orbitAtomMap hφ b).get ⋯

theorem ConNF.BaseLAction.orbitAtomMap_apply_ne [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) ⦃a : ConNF.Atom⦄ ⦃b : ConNF.Atom⦄ (ha : (φ.atomMap a).Dom) (hb : b ∈ φ.nextImageDomain hφ) :

(φ.orbitAtomMap hφ a).get ⋯ ≠ (φ.orbitAtomMap hφ b).get ⋯

theorem ConNF.BaseLAction.orbitAtomMap_injective [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) ⦃a : ConNF.Atom⦄ ⦃b : ConNF.Atom⦄ (ha : (φ.orbitAtomMap hφ a).Dom) (hb : (φ.orbitAtomMap hφ b).Dom) (h : (φ.orbitAtomMap hφ a).get ha = (φ.orbitAtomMap hφ b).get hb) :

a = b

theorem ConNF.BaseLAction.nextImageCore_atom_mem_litter_map [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : a ∈ φ.nextImageCoreDomain hφ) :

φ.nextImageCore hφ a a.1 ⋯ ∈ ConNF.litterSet ((φ.litterPerm hφ).toFun a.1)

theorem ConNF.BaseLAction.nextImageCore_not_mem_ran [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : a ∈ φ.nextImageCoreDomain hφ) :

φ.nextImageCore hφ a a.1 ⋯ ∉ φ.atomMap.ran

theorem ConNF.BaseLAction.nextImageCore_atom_mem [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (hdiff : ∀ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), symmDiff (↑((φ.litterMap L).get hL)) (ConNF.litterSet ((φ.litterMap L).get hL).fst) ⊆ φ.atomMap.ran) (a : ConNF.Atom) (ha : a ∈ φ.nextImageCoreDomain hφ) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) :

a.1 = L ↔ φ.nextImageCore hφ a a.1 ⋯ ∈ (φ.litterMap L).get hL

theorem ConNF.BaseLAction.orbitSetEquiv_atom_mem [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (hdiff : ∀ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), symmDiff (↑((φ.litterMap L).get hL)) (ConNF.litterSet ((φ.litterMap L).get hL).fst) ⊆ φ.atomMap.ran) (a : ConNF.Atom) (ha : a ∈ φ.needForwardImages ∧ a.1 ∈ (φ.litterPerm hφ).domain) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) :

a.1 = L ↔ ↑((φ.orbitSetEquiv ((φ.litterPerm hφ).toFun a.1)).symm (Sum.inr (0, ⟨a, ⋯⟩))) ∈ (φ.litterMap L).get hL

theorem ConNF.BaseLAction.orbit_atom_mem [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (hdiff : ∀ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), symmDiff (↑((φ.litterMap L).get hL)) (ConNF.litterSet ((φ.litterMap L).get hL).fst) ⊆ φ.atomMap.ran) (a : ConNF.Atom) (ha : (φ.orbitAtomMap hφ a).Dom) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) :

a.1 = L ↔ (φ.orbitAtomMap hφ a).get ha ∈ (φ.litterMap L).get hL

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

ConNF.BaseLAction

Extends an action by filling in orbits of atoms that act exceptionally with respect to litters in its domain.

Equations

φ.fillAtomOrbits hφ = { atomMap := φ.orbitAtomMap hφ, litterMap := φ.litterMap, atomMap_dom_small := ⋯, litterMap_dom_small := ⋯ }

Instances For

theorem ConNF.BaseLAction.fillAtomOrbitsLawful [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (hdiff : ∀ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), symmDiff (↑((φ.litterMap L).get hL)) (ConNF.litterSet ((φ.litterMap L).get hL).fst) ⊆ φ.atomMap.ran) :

(φ.fillAtomOrbits hφ).Lawful

@[simp]

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

(φ.fillAtomOrbits hφ).atomMap = φ.orbitAtomMap hφ

@[simp]

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

(φ.fillAtomOrbits hφ).litterMap = φ.litterMap

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

φ.atomMap.Dom ⊆ (φ.orbitAtomMap hφ).Dom

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

φ.atomMap.ran ⊆ (φ.orbitAtomMap hφ).ran

theorem ConNF.BaseLAction.fst_mem_litterPerm_domain_of_mem_map [ConNF.Params] {φ : ConNF.BaseLAction} (hφ : φ.Lawful) ⦃L : ConNF.Litter⦄ (hL : (φ.litterMap L).Dom) ⦃a : ConNF.Atom⦄ (ha : a ∈ (φ.litterMap L).get hL) :

a.1 ∈ (φ.litterPerm hφ).domain

theorem ConNF.BaseLAction.fst_mem_litterPerm_domain_of_dom [ConNF.Params] {φ : ConNF.BaseLAction} (hφ : φ.Lawful) ⦃a : ConNF.Atom⦄ (ha : a ∈ φ.atomMap.Dom) :

a.1 ∈ (φ.litterPerm hφ).domain

theorem ConNF.BaseLAction.fst_mem_litterPerm_domain_of_ran [ConNF.Params] {φ : ConNF.BaseLAction} (hφ : φ.Lawful) ⦃a : ConNF.Atom⦄ (ha : a ∈ φ.atomMap.ran) :

a.1 ∈ (φ.litterPerm hφ).domain

theorem ConNF.BaseLAction.fillAtomOrbits_precise [ConNF.Params] {φ : ConNF.BaseLAction} (hφ : φ.Lawful) (hdiff : ∀ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), symmDiff (↑((φ.litterMap L).get hL)) (ConNF.litterSet ((φ.litterMap L).get hL).fst) ⊆ φ.atomMap.ran) :

(φ.fillAtomOrbits hφ).Precise