Base litter actions

In this file, we define base litter actions.

Main declarations

• ConNF.BaseLAction: The type of base litter actions.
• ConNF.BaseLAction.Lawful: Injectivity requirements that allow a litter action to be converted into an approximation.
• ConNF.BaseLAction.Approximates: A base litter action approximates a base permutation if they agree wherever they are defined.

noncomputable def Or.elim' {α : Sort u_1} {p : Prop} {q : Prop} (h : p ∨ q) (f : p → α) (g : q → α) : α

Noncomputably eliminates a disjunction into a (possibly predicative) universe.

Equations

• h.elim' f g = if hp : p then f hp else g ⋯

theorem Or.elim'_left {α : Sort u_1} {p : Prop} {q : Prop} (h : p ∨ q) (f : p → α) (g : q → α) (hp : p) : h.elim' f g = f hp

theorem Or.elim'_right {α : Sort u_1} {p : Prop} {q : Prop} (h : p ∨ q) (f : p → α) (g : q → α) (hp : ¬p) : h.elim' f g = g ⋯

theorem ConNF.BaseLAction.ext_iff : ∀ {inst : ConNF.Params} (x y : ConNF.BaseLAction), x = y ↔ x.atomMap = y.atomMap ∧ x.litterMap = y.litterMap

theorem ConNF.BaseLAction.ext : ∀ {inst : ConNF.Params} (x y : ConNF.BaseLAction), x.atomMap = y.atomMap → x.litterMap = y.litterMap → x = y

structure ConNF.BaseLAction [ConNF.Params] : Type u

A base litter action is a partial function from atoms to atoms and a partial function from litters to near-litters, both of which have small domain. The image of a litter under the litter_map should be interpreted as the intended precise image of this litter under an allowable permutation.

• atomMap : ConNF.Atom →. ConNF.Atom
• litterMap : ConNF.Litter →. ConNF.NearLitter
• atomMap_dom_small : ConNF.Small self.atomMap.Dom
• litterMap_dom_small : ConNF.Small self.litterMap.Dom

theorem ConNF.BaseLAction.atomMap_dom_small [ConNF.Params] (self : ConNF.BaseLAction) : ConNF.Small self.atomMap.Dom

theorem ConNF.BaseLAction.litterMap_dom_small [ConNF.Params] (self : ConNF.BaseLAction) : ConNF.Small self.litterMap.Dom

structure ConNF.BaseLAction.Lawful [ConNF.Params] (φ : ConNF.BaseLAction) : Prop

A base litter action in which the atom and litter maps are injective (in suitable senses) and cohere in the sense that images of atoms in litters are mapped to atoms inside the corresponding near-litters.

• atomMap_injective : ∀ ⦃a b : ConNF.Atom⦄ (ha : (φ.atomMap a).Dom) (hb : (φ.atomMap b).Dom), (φ.atomMap a).get ha = (φ.atomMap b).get hb → a = b
• litterMap_injective : ∀ ⦃L₁ L₂ : ConNF.Litter⦄ (hL₁ : (φ.litterMap L₁).Dom) (hL₂ : (φ.litterMap L₂).Dom), (↑((φ.litterMap L₁).get hL₁) ∩ ↑((φ.litterMap L₂).get hL₂)).Nonempty → L₁ = L₂
• atom_mem : ∀ (a : ConNF.Atom) (ha : (φ.atomMap a).Dom) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), a.1 = L ↔ (φ.atomMap a).get ha ∈ (φ.litterMap L).get hL

theorem ConNF.BaseLAction.Lawful.atomMap_injective [ConNF.Params] {φ : ConNF.BaseLAction} (self : φ.Lawful) ⦃a : ConNF.Atom⦄ ⦃b : ConNF.Atom⦄ (ha : (φ.atomMap a).Dom) (hb : (φ.atomMap b).Dom) : (φ.atomMap a).get ha = (φ.atomMap b).get hb → a = b

theorem ConNF.BaseLAction.Lawful.litterMap_injective [ConNF.Params] {φ : ConNF.BaseLAction} (self : φ.Lawful) ⦃L₁ : ConNF.Litter⦄ ⦃L₂ : ConNF.Litter⦄ (hL₁ : (φ.litterMap L₁).Dom) (hL₂ : (φ.litterMap L₂).Dom) : (↑((φ.litterMap L₁).get hL₁) ∩ ↑((φ.litterMap L₂).get hL₂)).Nonempty → L₁ = L₂

theorem ConNF.BaseLAction.Lawful.atom_mem [ConNF.Params] {φ : ConNF.BaseLAction} (self : φ.Lawful) (a : ConNF.Atom) (ha : (φ.atomMap a).Dom) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : a.1 = L ↔ (φ.atomMap a).get ha ∈ (φ.litterMap L).get hL

theorem ConNF.BaseLAction.approximates_iff [ConNF.Params] (ψ : ConNF.BaseLAction) (π : ConNF.BasePerm) : ψ.Approximates π ↔ (∀ (a : ConNF.Atom) (h : (ψ.atomMap a).Dom), π • a = (ψ.atomMap a).get h) ∧ ∀ (L : ConNF.Litter) (h : (ψ.litterMap L).Dom), π • L.toNearLitter = (ψ.litterMap L).get h

structure ConNF.BaseLAction.Approximates [ConNF.Params] (ψ : ConNF.BaseLAction) (π : ConNF.BasePerm) : Prop

A base litter action approximates a base permutation if they agree wherever they are defined.

• map_atom : ∀ (a : ConNF.Atom) (h : (ψ.atomMap a).Dom), π • a = (ψ.atomMap a).get h
• map_litter : ∀ (L : ConNF.Litter) (h : (ψ.litterMap L).Dom), π • L.toNearLitter = (ψ.litterMap L).get h

theorem ConNF.BaseLAction.Approximates.map_atom [ConNF.Params] {ψ : ConNF.BaseLAction} {π : ConNF.BasePerm} (self : ψ.Approximates π) (a : ConNF.Atom) (h : (ψ.atomMap a).Dom) : π • a = (ψ.atomMap a).get h

theorem ConNF.BaseLAction.Approximates.map_litter [ConNF.Params] {ψ : ConNF.BaseLAction} {π : ConNF.BasePerm} (self : ψ.Approximates π) (L : ConNF.Litter) (h : (ψ.litterMap L).Dom) : π • L.toNearLitter = (ψ.litterMap L).get h

theorem ConNF.BaseLAction.bannedLitter_iff [ConNF.Params] (φ : ConNF.BaseLAction) : ∀ (a : ConNF.Litter), φ.BannedLitter a ↔ (∃ (a_1 : ConNF.Atom), (φ.atomMap a_1).Dom ∧ a = a_1.1) ∨ (φ.litterMap a).Dom ∨ (∃ (a_1 : ConNF.Atom) (h : (φ.atomMap a_1).Dom), a = ((φ.atomMap a_1).get h).1) ∨ (∃ (L : ConNF.Litter) (h : (φ.litterMap L).Dom), a = ((φ.litterMap L).get h).fst) ∨ ∃ (L : ConNF.Litter) (h : (φ.litterMap L).Dom), ∃ a_1 ∈ ↑((φ.litterMap L).get h) \ ConNF.litterSet ((φ.litterMap L).get h).fst, a = a_1.1

inductive ConNF.BaseLAction.BannedLitter [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.Litter → Prop

A litter that is not allowed to be used as a sandbox because it appears somewhere that we need to preserve.

• atomDom: ∀ [inst : ConNF.Params] {φ : ConNF.BaseLAction} (a : ConNF.Atom), (φ.atomMap a).Dom → φ.BannedLitter a.1
• litterDom: ∀ [inst : ConNF.Params] {φ : ConNF.BaseLAction} (L : ConNF.Litter), (φ.litterMap L).Dom → φ.BannedLitter L
• atomMap: ∀ [inst : ConNF.Params] {φ : ConNF.BaseLAction} (a : ConNF.Atom) (h : (φ.atomMap a).Dom), φ.BannedLitter ((φ.atomMap a).get h).1
• litterMap: ∀ [inst : ConNF.Params] {φ : ConNF.BaseLAction} (L : ConNF.Litter) (h : (φ.litterMap L).Dom), φ.BannedLitter ((φ.litterMap L).get h).fst
• diff: ∀ [inst : ConNF.Params] {φ : ConNF.BaseLAction} (L : ConNF.Litter) (h : (φ.litterMap L).Dom), ∀ a ∈ ↑((φ.litterMap L).get h) \ ConNF.litterSet ((φ.litterMap L).get h).fst, φ.BannedLitter a.1

theorem ConNF.BaseLAction.BannedLitter.memMap [ConNF.Params] (φ : ConNF.BaseLAction) (a : ConNF.Atom) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) (ha : a ∈ ↑((φ.litterMap L).get hL)) : φ.BannedLitter a.1

theorem ConNF.BaseLAction.bannedLitter_small [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.Small {L : ConNF.Litter | φ.BannedLitter L}

There are only a small amount of banned litters.

theorem ConNF.BaseLAction.mk_not_bannedLitter [ConNF.Params] (φ : ConNF.BaseLAction) : Cardinal.mk ↑{L : ConNF.Litter | ¬φ.BannedLitter L} = Cardinal.mk ConNF.μ

theorem ConNF.BaseLAction.not_bannedLitter_nonempty [ConNF.Params] (φ : ConNF.BaseLAction) : Nonempty ↑{L : ConNF.Litter | ¬φ.BannedLitter L}

noncomputable def ConNF.BaseLAction.atomMapOrElse [ConNF.Params] (φ : ConNF.BaseLAction) (a : ConNF.Atom) : ConNF.Atom

If a is in the domain, this is the atom map. Otherwise, this gives an arbitrary atom.

Equations

• φ.atomMapOrElse a = (φ.atomMap a).getOrElse (Classical.arbitrary ConNF.Atom)

theorem ConNF.BaseLAction.atomMapOrElse_of_dom [ConNF.Params] (φ : ConNF.BaseLAction) {a : ConNF.Atom} (ha : (φ.atomMap a).Dom) : φ.atomMapOrElse a = (φ.atomMap a).get ha

theorem ConNF.BaseLAction.atomMapOrElse_injective [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) : Set.InjOn φ.atomMapOrElse φ.atomMap.Dom

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

If L is in the domain, this is the litter map. Otherwise, this gives an arbitrary near-litter.

Equations

• φ.litterMapOrElse L = (φ.litterMap L).getOrElse (Classical.arbitrary ConNF.NearLitter)

theorem ConNF.BaseLAction.litterMapOrElse_of_dom [ConNF.Params] (φ : ConNF.BaseLAction) {L : ConNF.Litter} (hL : (φ.litterMap L).Dom) : φ.litterMapOrElse L = (φ.litterMap L).get hL

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

If L is in the domain, this gives the (rough) image of L under φ. Otherwise, this gives an arbitrary litter.

Equations

• φ.roughLitterMapOrElse L = (φ.litterMapOrElse L).fst

theorem ConNF.BaseLAction.roughLitterMapOrElse_of_dom [ConNF.Params] (φ : ConNF.BaseLAction) {L : ConNF.Litter} (hL : (φ.litterMap L).Dom) : φ.roughLitterMapOrElse L = ((φ.litterMap L).get hL).fst

Preorder structure

structure ConNF.BaseLAction.PFun.LE {α : Type u_1} {β : Type u_2} (f : α →. β) (g : α →. β) : Prop

We define that f ≤ g if the domain of f is included in the domain of g, and they agree where they are defined.

• dom_of_dom : ∀ (a : α), (f a).Dom → (g a).Dom
• get_eq : ∀ (a : α) (h : (f a).Dom), (f a).get h = (g a).get ⋯

theorem ConNF.BaseLAction.PFun.LE.dom_of_dom {α : Type u_1} {β : Type u_2} {f : α →. β} {g : α →. β} (self : ConNF.BaseLAction.PFun.LE f g) (a : α) : (f a).Dom → (g a).Dom

theorem ConNF.BaseLAction.PFun.LE.get_eq {α : Type u_1} {β : Type u_2} {f : α →. β} {g : α →. β} (self : ConNF.BaseLAction.PFun.LE f g) (a : α) (h : (f a).Dom) : (f a).get h = (g a).get ⋯

instance ConNF.BaseLAction.instPartialOrderPFun {α : Type u_1} {β : Type u_2} : PartialOrder (α →. β)

Equations

• ConNF.BaseLAction.instPartialOrderPFun = PartialOrder.mk ⋯

instance ConNF.BaseLAction.instPartialOrder [ConNF.Params] : PartialOrder ConNF.BaseLAction

Equations

• ConNF.BaseLAction.instPartialOrder = PartialOrder.mk ⋯

theorem ConNF.BaseLAction.Lawful.le [ConNF.Params] {φ : ConNF.BaseLAction} {ψ : ConNF.BaseLAction} (h : φ.Lawful) (hψ : ψ ≤ φ) : ψ.Lawful

theorem ConNF.BaseLAction.preciseAt_iff [ConNF.Params] (φ : ConNF.BaseLAction) ⦃L : ConNF.Litter⦄ (hL : (φ.litterMap L).Dom) : φ.PreciseAt hL ↔ symmDiff (↑((φ.litterMap L).get hL)) (ConNF.litterSet ((φ.litterMap L).get hL).fst) ⊆ φ.atomMap.ran ∧ (∀ (a : ConNF.Atom) (ha : (φ.atomMap a).Dom), (φ.atomMap a).get ha ∈ ConNF.litterSet L → (φ.atomMap ((φ.atomMap a).get ha)).Dom) ∧ φ.atomMap.Dom ∩ ↑((φ.litterMap L).get hL) ⊆ φ.atomMap.ran

structure ConNF.BaseLAction.PreciseAt [ConNF.Params] (φ : ConNF.BaseLAction) ⦃L : ConNF.Litter⦄ (hL : (φ.litterMap L).Dom) : Prop

An action is precise at a litter in its domain if all atoms in the symmetric difference of its image are accounted for.

• diff : symmDiff (↑((φ.litterMap L).get hL)) (ConNF.litterSet ((φ.litterMap L).get hL).fst) ⊆ φ.atomMap.ran
• fwd : ∀ (a : ConNF.Atom) (ha : (φ.atomMap a).Dom), (φ.atomMap a).get ha ∈ ConNF.litterSet L → (φ.atomMap ((φ.atomMap a).get ha)).Dom
• back : φ.atomMap.Dom ∩ ↑((φ.litterMap L).get hL) ⊆ φ.atomMap.ran

theorem ConNF.BaseLAction.PreciseAt.diff [ConNF.Params] {φ : ConNF.BaseLAction} {L : ConNF.Litter} {hL : (φ.litterMap L).Dom} (self : φ.PreciseAt hL) : symmDiff (↑((φ.litterMap L).get hL)) (ConNF.litterSet ((φ.litterMap L).get hL).fst) ⊆ φ.atomMap.ran

theorem ConNF.BaseLAction.PreciseAt.fwd [ConNF.Params] {φ : ConNF.BaseLAction} {L : ConNF.Litter} {hL : (φ.litterMap L).Dom} (self : φ.PreciseAt hL) (a : ConNF.Atom) (ha : (φ.atomMap a).Dom) : (φ.atomMap a).get ha ∈ ConNF.litterSet L → (φ.atomMap ((φ.atomMap a).get ha)).Dom

theorem ConNF.BaseLAction.PreciseAt.back [ConNF.Params] {φ : ConNF.BaseLAction} {L : ConNF.Litter} {hL : (φ.litterMap L).Dom} (self : φ.PreciseAt hL) : φ.atomMap.Dom ∩ ↑((φ.litterMap L).get hL) ⊆ φ.atomMap.ran

def ConNF.BaseLAction.Precise [ConNF.Params] (φ : ConNF.BaseLAction) : Prop

An action is precise if it is precise at every litter in its domain.

Equations

• φ.Precise = ∀ ⦃L : ConNF.Litter⦄ (hL : (φ.litterMap L).Dom), φ.PreciseAt hL

Induced litter permutation

theorem ConNF.BaseLAction.disjoint_dom_not_bannedLitter [ConNF.Params] (φ : ConNF.BaseLAction) : Disjoint (φ.litterMap.Dom ∪ φ.roughLitterMapOrElse '' φ.litterMap.Dom) {L : ConNF.Litter | ¬φ.BannedLitter L}

theorem ConNF.BaseLAction.roughLitterMapOrElse_injOn [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) : Set.InjOn φ.roughLitterMapOrElse φ.litterMap.Dom

theorem ConNF.BaseLAction.mk_not_bannedLitter_and_flexible [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} : Cardinal.mk ↑{L : ConNF.Litter | ¬φ.BannedLitter L ∧ ConNF.Flexible A L} = Cardinal.mk ConNF.μ

theorem ConNF.BaseLAction.mk_dom_inter_flexible_symmDiff_le [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} : Cardinal.mk ↑(symmDiff (φ.litterMap.Dom ∩ {L : ConNF.Litter | ConNF.Flexible A L}) (φ.roughLitterMapOrElse '' (φ.litterMap.Dom ∩ {L : ConNF.Litter | ConNF.Flexible A L}))) ≤ Cardinal.mk ↑{L : ConNF.Litter | ¬φ.BannedLitter L ∧ ConNF.Flexible A L}

theorem ConNF.BaseLAction.aleph0_le_not_bannedLitter_and_flexible [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} : Cardinal.aleph0 ≤ Cardinal.mk ↑{L : ConNF.Litter | ¬φ.BannedLitter L ∧ ConNF.Flexible A L}

theorem ConNF.BaseLAction.disjoint_dom_inter_flexible_not_bannedLitter [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} : Disjoint (φ.litterMap.Dom ∩ {L : ConNF.Litter | ConNF.Flexible A L} ∪ φ.roughLitterMapOrElse '' (φ.litterMap.Dom ∩ {L : ConNF.Litter | ConNF.Flexible A L})) {L : ConNF.Litter | ¬φ.BannedLitter L ∧ ConNF.Flexible A L}

theorem ConNF.BaseLAction.roughLitterMapOrElse_injOn_dom_inter_flexible [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (hφ : φ.Lawful) : Set.InjOn φ.roughLitterMapOrElse (φ.litterMap.Dom ∩ {L : ConNF.Litter | ConNF.Flexible A L})

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

A partial permutation that agrees with φ on flexible litters in its domain.

Equations

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

theorem ConNF.BaseLAction.flexibleLitterPartialPerm_apply_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {φ : ConNF.BaseLAction} {hφ : φ.Lawful} (L : ConNF.Litter) (hL₁ : L ∈ φ.litterMap.Dom) (hL₂ : ConNF.Flexible A L) : (φ.flexibleLitterPartialPerm hφ A).toFun L = φ.roughLitterMapOrElse L

theorem ConNF.BaseLAction.flexibleLitterPartialPerm_domain_small [ConNF.Params] (φ : ConNF.BaseLAction) [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (hφ : φ.Lawful) : ConNF.Small (φ.flexibleLitterPartialPerm hφ A).domain