digama0 · February 14, 2022 10:03 · Feb 14, 2022 · Feb 14, 2022
diff --git a/con_nf.lean b/con_nf.lean
@@ -134,6 +134,9 @@ class params :=
 (μ : Type u)
 (μ_limit : (#μ).is_strong_limit)
 (μ_cof : max (#Λ) (#κ) < (#μ).ord.cof)
+(δ : Λ)
+(hδ : (ordinal.typein Λr δ).is_limit)
+
 open params
 
 variable [params.{u}]
@@ -152,6 +155,9 @@ 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
@@ -246,13 +252,15 @@ 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 τ (A : xti) : Set := (symm_pow PI)^[2] (clan_Set A)
+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) (h : A.drop = some A') :
+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) (n) (hA : A.dropn n = some A') (hB : B.dropn n = some B')
-  (H : A.1 \ A'.1 = B.1 \ B'.1) :
+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
+end con_nf
diff --git a/con_nf.lean b/con_nf.lean
@@ -0,0 +1,258 @@
+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)
+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
+
+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 τ (A : xti) : Set := (symm_pow PI)^[2] (clan_Set A)
+
+theorem τ_power (A A' : xti) (h : A.drop = some A') :
+  symm_bij PI (τ PI A) (symm_pow PI (τ PI A')) := sorry
+
+theorem τ_elementary (A A' B B' : xti) (n) (hA : A.dropn n = some A') (hB : B.dropn n = some B')
+  (H : A.1 \ A'.1 = B.1 \ B'.1) :
+  bij ((symm_pow PI)^[n+2] (τ PI A')) ((symm_pow PI)^[n+2] (τ PI B')) := sorry
+
+end con_nf
No results found