ConNF.Background.PermutativeExtension

structure Rel.OrbitRestriction {α : Type u_1} (s : Set α) (β : Type u_2) :

Type (max u_1 u_2)

TODO: Fix the paper version of this.

sandbox : Set α
sandbox_disjoint : Disjoint s self.sandbox
categorise : α → β
catPerm : Equiv.Perm β
le_card_categorise (b : β) : max Cardinal.aleph0 (Cardinal.mk ↑s) ≤ Cardinal.mk ↑(self.sandbox ∩ self.categorise ⁻¹' {b})

Instances For

theorem Rel.le_card_categorise {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (b : β) :

Cardinal.mk (↑(r.dom ∪ r.codom) × ℕ) ≤ Cardinal.mk ↑(R.sandbox ∩ R.categorise ⁻¹' {b})

source

def Rel.catInj {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (b : β) :

↑(r.dom ∪ r.codom) × ℕ ↪ ↑(R.sandbox ∩ R.categorise ⁻¹' {b})

Equations

Rel.catInj R b = Nonempty.some ⋯

Instances For

source

theorem Rel.catInj_mem_sandbox {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (b : β) (x : ↑(r.dom ∪ r.codom) × ℕ) :

↑((catInj R b) x) ∈ R.sandbox

source

@[simp]

theorem Rel.categorise_catInj {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (b : β) (x : ↑(r.dom ∪ r.codom) × ℕ) :

R.categorise ↑((catInj R b) x) = b

source

theorem Rel.catInj_ne_of_mem {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (b : β) (x : ↑(r.dom ∪ r.codom) × ℕ) (a : α) (ha : a ∈ r.dom ∪ r.codom) :

↑((catInj R b) x) ≠ a

source

theorem Rel.catInj_injective {α : Type u_1} {β : Type u_2} {r : Rel α α} {R : OrbitRestriction (r.dom ∪ r.codom) β} {b₁ b₂ : β} {x₁ x₂ : ↑(r.dom ∪ r.codom) × ℕ} (h : ↑((catInj R b₁) x₁) = ↑((catInj R b₂) x₂)) :

b₁ = b₂ ∧ x₁ = x₂

source

@[simp]

theorem Rel.catInj_inj {α : Type u_1} {β : Type u_2} {r : Rel α α} {R : OrbitRestriction (r.dom ∪ r.codom) β} {b₁ b₂ : β} {a₁ a₂ : α} {h₁ : a₁ ∈ r.dom ∪ r.codom} {h₂ : a₂ ∈ r.dom ∪ r.codom} {n₁ n₂ : ℕ} :

↑((catInj R b₁) (⟨a₁, h₁⟩, n₁)) = ↑((catInj R b₂) (⟨a₂, h₂⟩, n₂)) ↔ b₁ = b₂ ∧ a₁ = a₂ ∧ n₁ = n₂

source

inductive Rel.newOrbits {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) :

Rel α α

left {α : Type u_1} {β : Type u_2} {r : Rel α α} {R : OrbitRestriction (r.dom ∪ r.codom) β} (a : α) (had : a ∈ r.dom) (hac : a ∉ r.codom) : newOrbits R (↑((catInj R ((Equiv.symm R.catPerm) (R.categorise a))) (⟨a, ⋯⟩, 0))) a
leftStep {α : Type u_1} {β : Type u_2} {r : Rel α α} {R : OrbitRestriction (r.dom ∪ r.codom) β} (n : ℕ) (a : α) (had : a ∈ r.dom) (hac : a ∉ r.codom) : newOrbits R ↑((catInj R ((⇑(Equiv.symm R.catPerm))^[n + 2] (R.categorise a))) (⟨a, ⋯⟩, n + 1)) ↑((catInj R ((⇑(Equiv.symm R.catPerm))^[n + 1] (R.categorise a))) (⟨a, ⋯⟩, n))
right {α : Type u_1} {β : Type u_2} {r : Rel α α} {R : OrbitRestriction (r.dom ∪ r.codom) β} (a : α) (had : a ∉ r.dom) (hac : a ∈ r.codom) : newOrbits R a ↑((catInj R (R.catPerm (R.categorise a))) (⟨a, ⋯⟩, 0))
rightStep {α : Type u_1} {β : Type u_2} {r : Rel α α} {R : OrbitRestriction (r.dom ∪ r.codom) β} (n : ℕ) (a : α) (had : a ∉ r.dom) (hac : a ∈ r.codom) : newOrbits R ↑((catInj R ((⇑R.catPerm)^[n + 1] (R.categorise a))) (⟨a, ⋯⟩, n)) ↑((catInj R ((⇑R.catPerm)^[n + 2] (R.categorise a))) (⟨a, ⋯⟩, n + 1))

Instances For

source

def Rel.permutativeExtension {α : Type u_1} {β : Type u_2} (r : Rel α α) (R : OrbitRestriction (r.dom ∪ r.codom) β) :

Rel α α

Equations

r.permutativeExtension R = r ⊔ Rel.newOrbits R

Instances For

source

theorem Rel.le_permutativeExtension {α : Type u_1} {β : Type u_2} (r : Rel α α) (R : OrbitRestriction (r.dom ∪ r.codom) β) :

r ≤ r.permutativeExtension R

source

theorem Rel.dom_permutativeExtension_subset {α : Type u_1} {β : Type u_2} (r : Rel α α) (R : OrbitRestriction (r.dom ∪ r.codom) β) :

(r.permutativeExtension R).dom ⊆ r.dom ∪ r.codom ∪ R.sandbox

source

theorem Rel.dom_permutativeExtension_subset' {α : Type u_1} {β : Type u_2} (r : Rel α α) (R : OrbitRestriction (r.dom ∪ r.codom) β) :

(r.permutativeExtension R).dom ⊆ r.dom ∪ r.codom ∪ ((⋃ a ∈ r.dom, ⋃ (n : ℕ), Subtype.val '' Set.range ⇑(catInj R ((⇑(Equiv.symm R.catPerm))^[n + 1] (R.categorise a)))) ∪ ⋃ a ∈ r.codom, ⋃ (n : ℕ), Subtype.val '' Set.range ⇑(catInj R ((⇑R.catPerm)^[n + 1] (R.categorise a))))

source

theorem Rel.card_permutativeExtension {α : Type u_1} {β : Type u_2} (r : Rel α α) (R : OrbitRestriction (r.dom ∪ r.codom) β) (hr : r.Coinjective) :

Cardinal.mk ↑(r.permutativeExtension R).dom ≤ max Cardinal.aleph0 (Cardinal.mk ↑r.dom)

source

theorem Rel.categorise_newOrbits {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) {a₁ a₂ : α} (h : newOrbits R a₁ a₂) :

R.categorise a₂ = R.catPerm (R.categorise a₁)

source

theorem Rel.categorise_permutativeExtension {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) {a₁ a₂ : α} (h : r.permutativeExtension R a₁ a₂) :

r a₁ a₂ ∨ R.categorise a₂ = R.catPerm (R.categorise a₁)

source

theorem Rel.newOrbits_injective {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) :

(newOrbits R).Injective

source

theorem Rel.newOrbits_coinjective {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) :

(newOrbits R).Coinjective

source

theorem Rel.newOrbits_oneOne {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) :

(newOrbits R).OneOne

source

theorem Rel.permutativeExtension_codomEqDom {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) :

(r.permutativeExtension R).CodomEqDom

source

theorem Rel.disjoint_newOrbits_dom {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) :

Disjoint r.dom (newOrbits R).dom

source

theorem Rel.disjoint_newOrbits_codom {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) :

Disjoint r.codom (newOrbits R).codom

source

theorem Rel.permutativeExtension_permutative {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (hr : r.OneOne) :

(r.permutativeExtension R).Permutative

source

theorem Rel.categorise_permutativeExtension_of_oneOne {α : Type u_1} {β : Type u_2} {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (hr : r.OneOne) {a₁ a₂ : α} (h : r.permutativeExtension R a₁ a₂) :

r a₁ a₂ ∨ a₁ ∉ r.dom ∧ a₂ ∉ r.codom ∧ R.categorise a₂ = R.catPerm (R.categorise a₁)

TODO: Strengthen statement in blueprint version.

source

def Rel.permutativeExtension' {α : Type u_1} (r : Rel α α) (hr : r.OneOne) (s : Set α) (hs₁ : s.Infinite) (hs₂ : Cardinal.mk ↑r.dom ≤ Cardinal.mk ↑s) (hs₃ : Disjoint (r.dom ∪ r.codom) s) :

Rel α α

Equations

r.permutativeExtension' hr s hs₁ hs₂ hs₃ = r.permutativeExtension { sandbox := s, sandbox_disjoint := hs₃, categorise := fun (x : α) => (), catPerm := 1, le_card_categorise := ⋯ }

Instances For

source

theorem Rel.le_permutativeExtension' {α : Type u_1} {r : Rel α α} {hr : r.OneOne} {s : Set α} {hs₁ : s.Infinite} {hs₂ : Cardinal.mk ↑r.dom ≤ Cardinal.mk ↑s} {hs₃ : Disjoint (r.dom ∪ r.codom) s} :

r ≤ r.permutativeExtension' hr s hs₁ hs₂ hs₃

source

theorem Rel.permutativeExtension'_permutative {α : Type u_1} {r : Rel α α} {hr : r.OneOne} {s : Set α} {hs₁ : s.Infinite} {hs₂ : Cardinal.mk ↑r.dom ≤ Cardinal.mk ↑s} {hs₃ : Disjoint (r.dom ∪ r.codom) s} :

(r.permutativeExtension' hr s hs₁ hs₂ hs₃).Permutative

source

theorem Rel.dom_permutativeExtension'_subset {α : Type u_1} {r : Rel α α} {hr : r.OneOne} {s : Set α} {hs₁ : s.Infinite} {hs₂ : Cardinal.mk ↑r.dom ≤ Cardinal.mk ↑s} {hs₃ : Disjoint (r.dom ∪ r.codom) s} :

(r.permutativeExtension' hr s hs₁ hs₂ hs₃).dom ⊆ r.dom ∪ r.codom ∪ s