Skip to content

Instantly share code, notes, and snippets.

@digama0
Last active Feb 14, 2022
Embed
What would you like to do?
import set_theory.cofinality
import order.symm_diff
import group_theory.subgroup.basic
import group_theory.group_action.basic
noncomputable theory
open_locale cardinal classical
universes u v
namespace ZFA
inductive pSet (A : Type v) : Type (max (u+1) v)
| atom : A → pSet
| range {α : Type u} (A : α → pSet) : pSet
namespace pSet
def equiv {A} : pSet A → pSet A → Prop
| (atom a) y := atom a = y
| x (atom a) := x = atom a
| (range A) (range B) :=
(∀ a, ∃ b, equiv a (B b)) ∧ (∀ b, ∃ a, equiv a (B b))
def map {A B} (f : A → B) : pSet A → pSet B
| (atom a) := atom (f a)
| (range A) := range (λ x, map (A x))
instance (A : Type*) : mul_action (equiv.perm A) (pSet A) :=
{ smul := λ π x, x.map π, one_smul := sorry, mul_smul := sorry }
def atoms {A} : pSet A := range atom
protected def empty {A} : pSet A := @range A pempty (λ e, match e with end)
instance (A) : has_emptyc (pSet A) := ⟨pSet.empty⟩
def type {A} : pSet A → Type u
| (atom a) := pempty
| (@range _ α A) := α
def func {A} : Π (x : pSet A), x.type → pSet A
| (atom a) := pempty.elim
| (range A) := A
protected def insert {A} (x y : pSet A) : pSet A :=
range (λ o, option.rec x y.func o)
instance (A) : has_insert (pSet A) (pSet A) := ⟨pSet.insert⟩
instance (A) : has_singleton (pSet A) (pSet A) := ⟨λ s, insert s ∅⟩
instance (A) : is_lawful_singleton (pSet A) (pSet A) := ⟨λ _, rfl⟩
def pair {A} (x y : pSet A) : pSet A := {{x}, {x, y}}
def powerset {A} (x : pSet A) : pSet A :=
range (λ p : set x.type, range (λ y : {a // p a}, x.func y))
protected def sep {A} (x : pSet A) (p : pSet A → Prop) : pSet A :=
range (λ y : {a // p (x.func a)}, x.func y)
def image {A} (f : pSet A → pSet A) (c : pSet A) : pSet A :=
range (λ a, f (c.func a))
end pSet
def Set (A) : Type* := quotient ⟨@pSet.equiv A, sorry
def Set.mk {A} : pSet A → Set A := quotient.mk'
def Set.map {A B} (f : A → B) (x : Set A) : Set B :=
quotient.lift_on' x (λ x, Set.mk (x.map f)) sorry
instance (A : Type*) : mul_action (equiv.perm A) (Set A) :=
{ smul := λ π x, x.map π, one_smul := sorry, mul_smul := sorry }
protected def empty {A} : Set A := Set.mk ∅
instance (A) : has_emptyc (Set A) := ⟨ZFA.empty⟩
protected def insert {A} (x y : Set A) : Set A :=
quotient.lift_on₂' x y (λ x y, Set.mk (x.insert y)) sorry
instance (A) : has_insert (Set A) (Set A) := ⟨ZFA.insert⟩
instance (A) : has_singleton (Set A) (Set A) := ⟨λ s, insert s ∅⟩
instance (A) : is_lawful_singleton (Set A) (Set A) := ⟨λ _, rfl⟩
def Set.is_bijection {A} (F x y : Set A) : Prop :=
∃ α (f g : α → pSet A),
function.injective (λ a, Set.mk (f a)) ∧ x = Set.mk (pSet.range f) ∧
function.injective (λ a, Set.mk (g a)) ∧ y = Set.mk (pSet.range g) ∧
F = Set.mk (pSet.range (λ a, (f a).pair (g a)))
def Set.bijective {A} (x y : Set A) : Prop := ∃ F, Set.is_bijection F x y
structure normal_filter {A : Type*} (G : subgroup (equiv.perm A)) :=
(Γ : set (subgroup (equiv.perm A)))
(is_perm : ∀ (K ∈ Γ), K ≤ G)
(atoms : ∀ a : A, mul_action.stabilizer (equiv.perm A) a ∈ Γ)
(upward : ∀ H K, H ∈ Γ → H ≤ K → K ∈ Γ)
(inter : ∀ H K, H ∈ Γ → K ∈ Γ → H ⊓ K ∈ Γ)
(conj : ∀ (π ∈ G) (h ∈ Γ), (h:subgroup _).map (mul_aut.conj π).to_monoid_hom ∈ Γ)
def Set.symmetric {A G} (F : @normal_filter A G) (x : Set A) : Prop :=
mul_action.stabilizer (equiv.perm A) x ∈ F.Γ
def pSet.symmetric {A G} (F : @normal_filter A G) (x : pSet A) : Prop := (Set.mk x).symmetric F
def pSet.hereditarily_symmetric {A G} (F : @normal_filter A G) : pSet A → Prop
| (pSet.atom a) := true
| x@(pSet.range f) := pSet.symmetric F x ∧ ∀ a, pSet.hereditarily_symmetric (f a)
def Set.hereditarily_symmetric {A G} (F : @normal_filter A G) (x : Set A) : Prop :=
quotient.lift_on' x (pSet.hereditarily_symmetric F) sorry
def pSet.symm_pow {A G} (F : @normal_filter A G) (x : pSet A) : pSet A :=
x.powerset.sep $ pSet.symmetric F
def Set.symm_pow {A G} (F : @normal_filter A G) (x : Set A) : Set A :=
quotient.lift_on' x (λ x, Set.mk (x.symm_pow F)) sorry
def Set.symm_bijective {A G} (F : @normal_filter A G) (x y : Set A) : Prop :=
∃ f, Set.is_bijection f x y ∧ Set.symmetric F f
end ZFA
namespace con_nf
class params :=
(Λ : Type u) (Λr : Λ → Λ → Prop) [Λwf : is_well_order Λ Λr]
(hΛ : (ordinal.type Λr).is_limit)
(κ : Type u) (hκ : (#κ).is_regular)
(μ : Type u)
(μ_limit : (#μ).is_strong_limit)
(μ_cof : max (#Λ) (#κ) < (#μ).ord.cof)
(δ : Λ)
(hδ : (ordinal.typein Λr δ).is_limit)
open params
variable [params.{u}]
def small {α} (x : set α) := #x < #κ
instance : is_well_order Λ Λr := Λwf
instance : linear_order Λ := linear_order_of_STO' Λr
-- extended type index
def xti : Type* := {s : finset Λ // s.nonempty}
def xti.min (s : xti) : Λ := s.1.min' s.2
def xti.max (s : xti) : Λ := s.1.max' s.2
def xti.drop (s : xti) : option xti := if h : _ then some ⟨s.1.erase s.min, h⟩ else none
def xti.drop_max (s : xti) : option xti := if h : _ then some ⟨s.1.erase s.max, h⟩ else none
instance : has_singleton Λ xti := ⟨λ x, ⟨{x}, finset.singleton_nonempty _⟩⟩
instance : has_insert Λ xti := ⟨λ x s, ⟨insert x s.1, finset.insert_nonempty _ _⟩⟩
noncomputable def xti.dropn (s : xti) : ℕ → option xti
| 0 := some s
| (n+1) := xti.dropn n >>= xti.drop
def clan (A : xti) := μ × κ
def atoms := Σ A, clan A
abbreviation pSet := ZFA.pSet atoms
abbreviation Set := ZFA.Set atoms
def atom {A} (x : clan A) : pSet := ZFA.pSet.atom ⟨A, x⟩
def clan_pSet (A : xti) : pSet := ZFA.pSet.range (@atom _ A)
def clan_Set (A : xti) : Set := ZFA.Set.mk (clan_pSet A)
def is_near_litter {A} (N : set (clan A)) := ∃ x : μ, small (N Δ {p:clan A | p.1 = x})
def near_litter (A) := {N : set (clan A) // is_near_litter N}
def near_litter_pSet {A} (N : near_litter A) : pSet :=
ZFA.pSet.range (λ x : N.1, atom x.1)
def near_litter.near {A} (N : near_litter A) : set (clan A) := {p:clan A | p.1 = N.2.some}
def local_card {A} (N : near_litter A) : set (near_litter A) :=
{M : near_litter A | M.near = N.near}
def local_card_pSet {A} (N : near_litter A) : pSet :=
ZFA.pSet.range (λ M : {M : near_litter A // M.near = N.near}, near_litter_pSet M.1)
def local_cards (A) : set (set (near_litter A)) := set.range local_card
def local_cards_pSet (A : xti) : pSet := ZFA.pSet.range (@local_card_pSet _ A)
def local_cards_Set (A : xti) : Set := ZFA.Set.mk (local_cards_pSet A)
def sdom : xti → xti → Prop
| A := λ B, A.max < B.max ∨ A.max = B.max ∧
∀ A' ∈ A.drop_max, ∃ B' ∈ B.drop_max,
have (A':xti).1.card < A.1.card, from sorry,
sdom A' B'
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ A, A.1.card)⟩]}
instance : has_lt xti := ⟨sdom⟩
instance : is_well_order xti (<) := sorry
variables {P : xti → Prop} (PI : ∀ B, P B → Set)
def allowable' : subgroup (equiv.perm atoms) :=
(⨅ B (h : P B), mul_action.stabilizer _ (PI B h)) ⊓
⨅ C, mul_action.stabilizer _ (local_cards_Set C)
def A_allowable (A) (PI : ∀ B, B < A → Set) : subgroup (equiv.perm atoms) :=
allowable' PI
def support_el := Σ A, clan A ⊕ near_litter A
def support_el.inr (A) (N : near_litter A) : support_el := ⟨A, sum.inr N⟩
structure support_order :=
(S : set support_el)
(small : small S)
(disj (A M N) : support_el.inr A M ∈ S → support_el.inr A N ∈ S → M ≠ N → disjoint M.1 N.1)
(r : S → S → Prop)
(wo : is_well_order S r)
def supported' (S : support_order) : subgroup (equiv.perm atoms) :=
allowable' PI ⊓
⨅ a ∈ S.S, match a with
| ⟨A, sum.inl c⟩ := mul_action.stabilizer _ (@id atoms ⟨A, c⟩)
| ⟨A, sum.inr N⟩ := mul_action.stabilizer _ (near_litter_pSet N)
end
def has_support' (S : support_order)
{α} [mul_action (equiv.perm atoms) α] (x : α) : Prop :=
supported' PI S ≤ mul_action.stabilizer (equiv.perm atoms) x
def is_symmetric' {P : xti → Prop} (PI : ∀ B, P B → Set)
{α} [mul_action (equiv.perm atoms) α] (x : α) : Prop :=
∃ S, has_support' PI S x
def support_filter' : ZFA.normal_filter (allowable' PI) :=
{ Γ := {K | ∃ S, supported' PI S ≤ K},
is_perm := sorry,
atoms := sorry,
upward := sorry,
inter := sorry,
conj := sorry }
variable (PI_sym : ∀ B (h : P B), ZFA.Set.symmetric (support_filter' PI) (PI B h))
def symm_pow : Set → Set := ZFA.Set.symm_pow (support_filter' PI)
def symm_bij : Set → Set → Prop := ZFA.Set.symm_bijective (support_filter' PI)
def bij : Set → Set → Prop := ZFA.Set.bijective
def xti_below := {A : xti // A < {δ}}
def τ (A : xti_below) : Set := (symm_pow PI)^[2] (clan_Set (insert δ A.1))
theorem τ_power (A A' : xti_below) (h : A.1.drop = some A'.1) :
symm_bij PI (τ PI A) (symm_pow PI (τ PI A')) := sorry
theorem τ_elementary (A A' B B' : xti_below) (n)
(hA : A.1.dropn n = some A'.1) (hB : B.1.dropn n = some B'.1)
(H : A.1.1 \ A'.1.1 = B.1.1 \ B'.1.1) :
bij ((symm_pow PI)^[n+2] (τ PI A')) ((symm_pow PI)^[n+2] (τ PI B')) := sorry
end con_nf
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment