Base approximations

In this file, we define base approximations.

Main declarations

• ConNF.BaseApprox: A base approximation consists of a partial permutation of atoms and a partial permutation of near-litters.

structure ConNF.BaseApprox [Params] : Type u

• exceptions : Rel Atom Atom
• litters : Rel Litter Litter
• exceptions_permutative : self.exceptions.Permutative
• litters_permutative' : self.litters.Permutative
• exceptions_small (L : Litter) : Small (Lᴬ ∩ self.exceptions.dom)

instance ConNF.BaseApprox.instSuperLRelLitter [Params] : SuperL BaseApprox (Rel Litter Litter)

Equations

• ConNF.BaseApprox.instSuperLRelLitter = { superL := ConNF.BaseApprox.litters }

@[simp]

theorem ConNF.BaseApprox.mk_litters [Params] (exceptions : Rel Atom Atom) (litters : Rel Litter Litter) (exceptions_permutative : exceptions.Permutative) (litters_permutative' : litters.Permutative) (exceptions_small : ∀ (L : Litter), Small (Lᴬ ∩ exceptions.dom)) : { exceptions := exceptions, litters := litters, exceptions_permutative := exceptions_permutative, litters_permutative' := litters_permutative', exceptions_small := exceptions_small }ᴸ = litters

theorem ConNF.BaseApprox.ext [Params] {ψ χ : BaseApprox} (h₁ : ψ.exceptions = χ.exceptions) (h₂ : ψᴸ = χᴸ) : ψ = χ

theorem ConNF.BaseApprox.litters_permutative [Params] (ψ : BaseApprox) : ψᴸ.Permutative

instance ConNF.BaseApprox.instInv [Params] : Inv BaseApprox

Equations

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

@[simp]

theorem ConNF.BaseApprox.inv_exceptions [Params] (ψ : BaseApprox) : ψ⁻¹.exceptions = ψ.exceptions.inv

@[simp]

theorem ConNF.BaseApprox.inv_litters [Params] (ψ : BaseApprox) : ψ⁻¹ᴸ = ψᴸ.inv

@[simp]

theorem ConNF.BaseApprox.inv_inv [Params] (ψ : BaseApprox) : ψ⁻¹⁻¹ = ψ

def ConNF.BaseApprox.sublitterAtoms [Params] (ψ : BaseApprox) (L : Litter) : Set Atom

Equations

• ψ.sublitterAtoms L = Lᴬ \ ψ.exceptions.dom

theorem ConNF.BaseApprox.sublitterAtoms_near [Params] (ψ : BaseApprox) (L : Litter) : ψ.sublitterAtoms L ~ Lᴬ

def ConNF.BaseApprox.sublitter [Params] (ψ : BaseApprox) (L : Litter) : NearLitter

Equations

• ψ.sublitter L = { litter := L, atoms := ψ.sublitterAtoms L, atoms_near_litter' := ⋯ }

theorem ConNF.BaseApprox.sublitter_atoms [Params] {ψ : BaseApprox} {L : Litter} : (ψ.sublitter L)ᴬ = Lᴬ \ ψ.exceptions.dom

theorem ConNF.BaseApprox.sublitter_subset [Params] {ψ : BaseApprox} {L : Litter} : (ψ.sublitter L)ᴬ ⊆ Lᴬ

theorem ConNF.BaseApprox.sublitter_atoms_disjoint [Params] {ψ : BaseApprox} {L : Litter} : Disjoint (ψ.sublitter L)ᴬ ψ.exceptions.dom

@[simp]

theorem ConNF.BaseApprox.inv_sublitter [Params] (ψ : BaseApprox) (L : Litter) : ψ⁻¹.sublitter L = ψ.sublitter L

def ConNF.BaseApprox.nearLitterEquiv [Params] (N : NearLitter) : κ ≃ ↑Nᴬ

Equations

• ConNF.BaseApprox.nearLitterEquiv N = ⋯.some

theorem ConNF.BaseApprox.nearLitterEquiv_injective [Params] {N : NearLitter} {i₁ i₂ : κ} (h : ↑((nearLitterEquiv N) i₁) = ↑((nearLitterEquiv N) i₂)) : i₁ = i₂

theorem ConNF.BaseApprox.nearLitterEquiv_congr [Params] {N₁ N₂ : NearLitter} {i₁ i₂ : κ} (hN : N₁ = N₂) (hi : i₁ = i₂) : ↑((nearLitterEquiv N₁) i₁) = ↑((nearLitterEquiv N₂) i₂)

theorem ConNF.BaseApprox.nearLitterEquiv_mem [Params] (N : NearLitter) (i : κ) : ↑((nearLitterEquiv N) i) ∈ Nᴬ

@[simp]

theorem ConNF.BaseApprox.nearLitterEquiv_litter [Params] (ψ : BaseApprox) (L : Litter) (i : κ) : (↑((nearLitterEquiv (ψ.sublitter L)) i))ᴸ = L

theorem ConNF.BaseApprox.nearLitterEquiv_not_mem_dom [Params] (ψ : BaseApprox) (L : Litter) (i : κ) : ↑((nearLitterEquiv (ψ.sublitter L)) i) ∉ ψ.exceptions.dom

inductive ConNF.BaseApprox.typical [Params] (ψ : BaseApprox) : Rel Atom Atom

• mk [Params] {ψ : BaseApprox} (L₁ L₂ : Litter) (h : ψᴸ L₁ L₂) (i : κ) : ψ.typical ↑((nearLitterEquiv (ψ.sublitter L₁)) i) ↑((nearLitterEquiv (ψ.sublitter L₂)) i)

theorem ConNF.BaseApprox.typical_iff [Params] {ψ : BaseApprox} {a₁ a₂ : Atom} : ψ.typical a₁ a₂ ↔ ψᴸ a₁ᴸ a₂ᴸ ∧ ∃ (i : κ), a₁ = ↑((nearLitterEquiv (ψ.sublitter a₁ᴸ)) i) ∧ a₂ = ↑((nearLitterEquiv (ψ.sublitter a₂ᴸ)) i)

theorem ConNF.BaseApprox.not_mem_dom_of_typical [Params] {ψ : BaseApprox} {a₁ a₂ : Atom} (h : ψ.typical a₁ a₂) : a₁ ∉ ψ.exceptions.dom

theorem ConNF.BaseApprox.typical_inv_of_typical [Params] {ψ : BaseApprox} {a₁ a₂ : Atom} (h : ψ.typical a₁ a₂) : ψ⁻¹.typical a₂ a₁

theorem ConNF.BaseApprox.typical_inv_iff_typical [Params] {ψ : BaseApprox} {a₁ a₂ : Atom} : ψ⁻¹.typical a₂ a₁ ↔ ψ.typical a₁ a₂

@[simp]

theorem ConNF.BaseApprox.inv_typical [Params] {ψ : BaseApprox} : ψ⁻¹.typical = ψ.typical.inv

def ConNF.BaseApprox.atoms [Params] (ψ : BaseApprox) : Rel Atom Atom

Equations

• ψ.atoms = ψ.exceptions ⊔ ψ.typical

instance ConNF.BaseApprox.instSuperARelAtom [Params] : SuperA BaseApprox (Rel Atom Atom)

Equations

• ConNF.BaseApprox.instSuperARelAtom = { superA := ConNF.BaseApprox.atoms }

theorem ConNF.BaseApprox.atoms_def [Params] (ψ : BaseApprox) : ψᴬ = ψ.exceptions ⊔ ψ.typical

theorem ConNF.BaseApprox.exceptions_le_atoms [Params] (ψ : BaseApprox) : ψ.exceptions ≤ ψᴬ

theorem ConNF.BaseApprox.exceptions_dom_subset_atoms_dom [Params] (ψ : BaseApprox) : ψ.exceptions.dom ⊆ ψᴬ.dom

theorem ConNF.BaseApprox.mem_dom_atoms_of_litter_mem_dom [Params] {ψ : BaseApprox} {a : Atom} (h : aᴸ ∈ ψᴸ.dom) : a ∈ ψᴬ.dom

@[simp]

theorem ConNF.BaseApprox.inv_atoms [Params] (ψ : BaseApprox) : ψ⁻¹ᴬ = ψᴬ.inv

theorem ConNF.BaseApprox.typical_injective [Params] (ψ : BaseApprox) : ψ.typical.Injective

theorem ConNF.BaseApprox.typical_coinjective [Params] (ψ : BaseApprox) : ψ.typical.Coinjective

theorem ConNF.BaseApprox.typical_codomEqDom [Params] (ψ : BaseApprox) : ψ.typical.CodomEqDom

theorem ConNF.BaseApprox.typical_permutative [Params] (ψ : BaseApprox) : ψ.typical.Permutative

theorem ConNF.BaseApprox.exceptions_typical_disjoint [Params] (ψ : BaseApprox) : Disjoint ψ.exceptions.dom ψ.typical.dom

theorem ConNF.BaseApprox.atoms_permutative [Params] (ψ : BaseApprox) : ψᴬ.Permutative

theorem ConNF.BaseApprox.atoms_image_eq_typical_image [Params] (ψ : BaseApprox) {s : Set Atom} (hs : Disjoint ψ.exceptions.dom s) : ψᴬ.image s = ψ.typical.image s

theorem ConNF.BaseApprox.typical_image_sublitter [Params] (ψ : BaseApprox) {L₁ L₂ : Litter} (h : ψᴸ L₁ L₂) : ψ.typical.image (ψ.sublitter L₁)ᴬ = (ψ.sublitter L₂)ᴬ

theorem ConNF.BaseApprox.image_near_of_near [Params] (ψ : BaseApprox) (s : Set Atom) {L₁ L₂ : Litter} (hL : ψᴸ L₁ L₂) (hsL : s ~ L₁ᴬ) : ψᴬ.image s ~ L₂ᴬ

def ConNF.BaseApprox.nearLitters [Params] (ψ : BaseApprox) : Rel NearLitter NearLitter

Equations

• ψ.nearLitters N₁ N₂ = (ψᴸ N₁ᴸ N₂ᴸ ∧ N₁ᴬ ⊆ ψᴬ.dom ∧ ψᴬ.image N₁ᴬ = N₂ᴬ)

instance ConNF.BaseApprox.instSuperNRelNearLitter [Params] : SuperN BaseApprox (Rel NearLitter NearLitter)

Equations

• ConNF.BaseApprox.instSuperNRelNearLitter = { superN := ConNF.BaseApprox.nearLitters }

theorem ConNF.BaseApprox.nearLitters_def [Params] (ψ : BaseApprox) {N₁ N₂ : NearLitter} : ψᴺ N₁ N₂ ↔ ψᴸ N₁ᴸ N₂ᴸ ∧ N₁ᴬ ⊆ ψᴬ.dom ∧ ψᴬ.image N₁ᴬ = N₂ᴬ

theorem ConNF.BaseApprox.mem_dom_nearLitters [Params] {ψ : BaseApprox} {N : NearLitter} (hL : Nᴸ ∈ ψᴸ.dom) (ha : ∀ a ∈ Nᴬ \ Nᴸᴬ, a ∈ ψᴬ.dom) : N ∈ ψᴺ.dom

@[simp]

theorem ConNF.BaseApprox.inv_nearLitters [Params] (ψ : BaseApprox) : ψ⁻¹ᴺ = ψᴺ.inv

theorem ConNF.BaseApprox.atoms_subset_dom_of_nearLitters_left [Params] {ψ : BaseApprox} {N₁ N₂ : NearLitter} (h : ψᴺ N₁ N₂) : N₁ᴬ ⊆ ψᴬ.dom

theorem ConNF.BaseApprox.atoms_subset_dom_of_nearLitters_right [Params] {ψ : BaseApprox} {N₁ N₂ : NearLitter} (h : ψᴺ N₁ N₂) : N₂ᴬ ⊆ ψᴬ.dom

theorem ConNF.BaseApprox.nearLitters_injective [Params] (ψ : BaseApprox) : ψᴺ.Injective

theorem ConNF.BaseApprox.nearLitters_coinjective [Params] (ψ : BaseApprox) : ψᴺ.Coinjective

theorem ConNF.BaseApprox.nearLitters_codom_subset_dom [Params] (ψ : BaseApprox) : ψᴺ.codom ⊆ ψᴺ.dom

theorem ConNF.BaseApprox.nearLitters_permutative [Params] (ψ : BaseApprox) : ψᴺ.Permutative

instance ConNF.BaseApprox.instLE [Params] : LE BaseApprox

Equations

• ConNF.BaseApprox.instLE = { le := fun (ψ χ : ConNF.BaseApprox) => ψ.exceptions = χ.exceptions ∧ ψᴸ ≤ χᴸ }

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

Equations

• ConNF.BaseApprox.instPartialOrder = PartialOrder.mk ⋯

theorem ConNF.BaseApprox.litters_le_of_le [Params] {ψ χ : BaseApprox} (h : ψ ≤ χ) : ψᴸ ≤ χᴸ

theorem ConNF.BaseApprox.sublitter_eq_of_le [Params] {ψ χ : BaseApprox} (h : ψ ≤ χ) (L : Litter) : ψ.sublitter L = χ.sublitter L

theorem ConNF.BaseApprox.typical_le_of_le [Params] {ψ χ : BaseApprox} (h : ψ ≤ χ) : ψ.typical ≤ χ.typical

theorem ConNF.BaseApprox.atoms_le_of_le [Params] {ψ χ : BaseApprox} (h : ψ ≤ χ) : ψᴬ ≤ χᴬ

theorem ConNF.BaseApprox.nearLitters_le_of_le [Params] {ψ χ : BaseApprox} (h : ψ ≤ χ) : ψᴺ ≤ χᴺ

instance ConNF.BaseApprox.instBaseActionClass [Params] : BaseActionClass BaseApprox

This creates new definitions of ·ᴬ and ·ᴺ, but the instances are definitionally equal so no triangles are formed.

Equations

• ConNF.BaseApprox.instBaseActionClass = { atoms := fun (ψ : ConNF.BaseApprox) => ψᴬ, atoms_oneOne := ⋯, nearLitters := fun (ψ : ConNF.BaseApprox) => ψᴺ, nearLitters_oneOne := ⋯ }

def ConNF.BaseApprox.addOrbitLitters [Params] (f : ℤ → Litter) : Rel Litter Litter

Equations

• ConNF.BaseApprox.addOrbitLitters f L₁ L₂ = ∃ (n : ℤ), L₁ = f n ∧ L₂ = f (n + 1)

@[simp]

theorem ConNF.BaseApprox.addOrbitLitters_dom [Params] (f : ℤ → Litter) : (addOrbitLitters f).dom = Set.range f

theorem ConNF.BaseApprox.addOrbitLitters_codomEqDom [Params] (f : ℤ → Litter) : (addOrbitLitters f).CodomEqDom

theorem ConNF.BaseApprox.addOrbitLitters_oneOne [Params] (f : ℤ → Litter) (hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)) : (addOrbitLitters f).OneOne

theorem ConNF.BaseApprox.addOrbitLitters_permutative [Params] (f : ℤ → Litter) (hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)) : (addOrbitLitters f).Permutative

theorem ConNF.BaseApprox.disjoint_litters_dom_addOrbitLitters_dom [Params] (ψ : BaseApprox) (f : ℤ → Litter) (hfψ : ∀ (n : ℤ), f n ∉ ψᴸ.dom) : Disjoint ψᴸ.dom (addOrbitLitters f).dom

def ConNF.BaseApprox.addOrbit [Params] (ψ : BaseApprox) (f : ℤ → Litter) (hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)) (hfψ : ∀ (n : ℤ), f n ∉ ψᴸ.dom) : BaseApprox

Equations

• ψ.addOrbit f hf hfψ = { exceptions := ψ.exceptions, litters := ψ.litters ⊔ ConNF.BaseApprox.addOrbitLitters f, exceptions_permutative := ⋯, litters_permutative' := ⋯, exceptions_small := ⋯ }

theorem ConNF.BaseApprox.addOrbit_litters [Params] {ψ : BaseApprox} {f : ℤ → Litter} {hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ (n : ℤ), f n ∉ ψᴸ.dom} : (ψ.addOrbit f hf hfψ)ᴸ = ψᴸ ⊔ addOrbitLitters f

theorem ConNF.BaseApprox.le_addOrbit [Params] {ψ : BaseApprox} {f : ℤ → Litter} {hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ (n : ℤ), f n ∉ ψᴸ.dom} : ψ ≤ ψ.addOrbit f hf hfψ

theorem ConNF.BaseApprox.upperBound_exceptions_small [Params] (c : Set BaseApprox) (hc : IsChain (fun (x1 x2 : BaseApprox) => x1 ≤ x2) c) (L : Litter) : Small (Lᴬ ∩ (⨆ ψ ∈ c, ψ.exceptions).dom)

def ConNF.BaseApprox.upperBound [Params] (c : Set BaseApprox) (hc : IsChain (fun (x1 x2 : BaseApprox) => x1 ≤ x2) c) : BaseApprox

An upper bound for a chain of base approximations.

Equations

• ConNF.BaseApprox.upperBound c hc = { exceptions := ⨆ ψ ∈ c, ψ.exceptions, litters := ⨆ ψ ∈ c, ψᴸ, exceptions_permutative := ⋯, litters_permutative' := ⋯, exceptions_small := ⋯ }

theorem ConNF.BaseApprox.le_upperBound [Params] (c : Set BaseApprox) (hc : IsChain (fun (x1 x2 : BaseApprox) => x1 ≤ x2) c) (ψ : BaseApprox) : ψ ∈ c → ψ ≤ upperBound c hc

def ConNF.BaseApprox.Total [Params] (ψ : BaseApprox) : Prop

Equations

• ψ.Total = ∀ (L : ConNF.Litter), L ∈ ψᴸ.dom

theorem ConNF.BaseApprox.Total.atoms [Params] {ψ : BaseApprox} (h : ψ.Total) (a : Atom) : a ∈ ψᴬ.dom

theorem ConNF.BaseApprox.Total.nearLitters [Params] {ψ : BaseApprox} (h : ψ.Total) (N : NearLitter) : N ∈ ψᴺ.dom

theorem ConNF.BaseApprox.Total.atoms_bijective [Params] {ψ : BaseApprox} (h : ψ.Total) : ψᴬ.Bijective

theorem ConNF.BaseApprox.Total.litters_bijective [Params] {ψ : BaseApprox} (h : ψ.Total) : ψᴸ.Bijective

theorem ConNF.BaseApprox.basePerm_apply_near_apply [Params] (ψ : BaseApprox) (h : ψ.Total) (s : Set Atom) (L : Litter) : s ~ Lᴬ → ⇑(ψᴬ.toEquiv ⋯) '' s ~ ((ψᴸ.toEquiv ⋯) L)ᴬ

def ConNF.BaseApprox.basePerm [Params] (ψ : BaseApprox) (h : ψ.Total) : BasePerm

Equations

• ψ.basePerm h = { atoms := ψᴬ.toEquiv ⋯, litters := ψᴸ.toEquiv ⋯, apply_near_apply := ⋯ }

theorem ConNF.BaseApprox.basePerm_smul_atom_def [Params] {ψ : BaseApprox} {h : ψ.Total} {a : Atom} : ψ.basePerm h • a = ψᴬ.toFunction ⋯ a

theorem ConNF.BaseApprox.basePerm_smul_litter_def [Params] {ψ : BaseApprox} {h : ψ.Total} {L : Litter} : ψ.basePerm h • L = ψᴸ.toFunction ⋯ L

@[simp]

theorem ConNF.BaseApprox.basePerm_smul_atom_eq_iff [Params] {ψ : BaseApprox} {h : ψ.Total} {a₁ a₂ : Atom} : ψ.basePerm h • a₁ = a₂ ↔ ψᴬ a₁ a₂

@[simp]

theorem ConNF.BaseApprox.basePerm_inv_smul_atom_eq_iff [Params] {ψ : BaseApprox} {h : ψ.Total} {a₁ a₂ : Atom} : (ψ.basePerm h)⁻¹ • a₁ = a₂ ↔ ψᴬ a₂ a₁

@[simp]

theorem ConNF.BaseApprox.basePerm_smul_litter_eq_iff [Params] {ψ : BaseApprox} {h : ψ.Total} {L₁ L₂ : Litter} : ψ.basePerm h • L₁ = L₂ ↔ ψᴸ L₁ L₂

@[simp]

theorem ConNF.BaseApprox.basePerm_inv_smul_litter_eq_iff [Params] {ψ : BaseApprox} {h : ψ.Total} {L₁ L₂ : Litter} : (ψ.basePerm h)⁻¹ • L₁ = L₂ ↔ ψᴸ L₂ L₁

@[simp]

theorem ConNF.BaseApprox.basePerm_smul_nearLitter_eq_iff [Params] {ψ : BaseApprox} {h : ψ.Total} {N₁ N₂ : NearLitter} : ψ.basePerm h • N₁ = N₂ ↔ ψᴺ N₁ N₂

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

• atoms (a₁ a₂ : Atom) : ψᴬ a₁ a₂ → a₂ = π • a₁
• nearLitters (N₁ N₂ : NearLitter) : ψᴺ N₁ N₂ → N₂ = π • N₁

theorem ConNF.BaseApprox.Approximates.litters [Params] {ψ : BaseApprox} {π : BasePerm} (h : ψ.Approximates π) (L₁ L₂ : Litter) : ψᴸ L₁ L₂ → π • L₁ = L₂

theorem ConNF.BaseApprox.Approximates.mono [Params] {ψ χ : BaseApprox} {π : BasePerm} (hχ : χ.Approximates π) (h : ψ ≤ χ) : ψ.Approximates π

structure ConNF.BaseApprox.ExactlyApproximates [Params] (ψ : BaseApprox) (π : BasePerm) extends ψ.Approximates π : Prop

• atoms (a₁ a₂ : Atom) : ψᴬ a₁ a₂ → a₂ = π • a₁
• nearLitters (N₁ N₂ : NearLitter) : ψᴺ N₁ N₂ → N₂ = π • N₁
• smul_litter (a : Atom) : a ∉ ψ.exceptions.dom → (π • a)ᴸ = π • aᴸ
• inv_smul_litter (a : Atom) : a ∉ ψ.exceptions.dom → (π⁻¹ • a)ᴸ = π⁻¹ • aᴸ

theorem ConNF.BaseApprox.ExactlyApproximates.mono [Params] {ψ χ : BaseApprox} {π : BasePerm} (hχ : χ.ExactlyApproximates π) (h : ψ ≤ χ) : ψ.ExactlyApproximates π

theorem ConNF.BaseApprox.ExactlyApproximates.smulSet_nearLitter [Params] {ψ : BaseApprox} {π : BasePerm} {N₁ N₂ : NearLitter} (hψ : ψ.ExactlyApproximates π) (hNπ : π • N₁ᴸ = N₂ᴸ) : π • (N₁ᴸᴬ \ ψ.exceptions.dom) = N₂ᴸᴬ \ ψ.exceptions.dom

theorem ConNF.BaseApprox.Approximates.smulSet_eq_exceptions_image [Params] {ψ : BaseApprox} {π : BasePerm} (hψ : ψ.Approximates π) (s : Set Atom) (hs : s ⊆ ψ.exceptions.dom) : π • s = ψ.exceptions.image s

theorem ConNF.BaseApprox.approximates_basePerm [Params] {ψ : BaseApprox} (h : ψ.Total) : ψ.Approximates (ψ.basePerm h)

theorem ConNF.BaseApprox.exactlyApproximates_basePerm [Params] {ψ : BaseApprox} (h : ψ.Total) : ψ.ExactlyApproximates (ψ.basePerm h)