Misere combinatorial games.

class MisereGames.Universe {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) extends MisereGames.Form.ClosedUnderAdd A, MisereGames.Form.Hereditary A, MisereGames.Form.ClosedUnderNeg A, MisereGames.ClosedUnderDicotic IsAmbient A : Prop

A universe is closed under addition, options, negation, and dicotic construction.

• has_add (g h : G) (h_g : A g) (h_h : A h) : A (g + h)
• has_option {g g' : G} (h1 : A g) (h2 : IsOption g' g) : A g'
• neg_of {g : G} (h1 : A g) : A (-g)
• closed_dicotic (B C : Set G) [Small.{u, u + 1} ↑B] [Small.{u, u + 1} ↑C] (hB : ∀ b ∈ B, A b) (hC : ∀ c ∈ C, A c) : B.Nonempty → C.Nonempty → IsAmbient !{B | C} → A !{B | C}
• zero_mem : A 0
• isAmbient_of_mem {g : G} : A g → IsAmbient g

class MisereGames.LongUniverse {G : Type (u + 1)} [Form G] (A : G → Prop) extends MisereGames.Universe MisereGames.Form.IsLong A : Prop

A universe in the long ambient space.

• has_add (g h : G) (h_g : A g) (h_h : A h) : A (g + h)
• has_option {g g' : G} (h1 : A g) (h2 : IsOption g' g) : A g'
• neg_of {g : G} (h1 : A g) : A (-g)
• closed_dicotic (B C : Set G) [Small.{u, u + 1} ↑B] [Small.{u, u + 1} ↑C] (hB : ∀ b ∈ B, A b) (hC : ∀ c ∈ C, A c) : B.Nonempty → C.Nonempty → Form.IsLong !{B | C} → A !{B | C}
• zero_mem : A 0
• isAmbient_of_mem {g : G} : A g → Form.IsLong g

class MisereGames.ShortUniverse {G : Type (u + 1)} [Form G] (A : G → Prop) extends MisereGames.Universe MisereGames.Form.IsShort A : Prop

A universe in the short ambient space.

• has_add (g h : G) (h_g : A g) (h_h : A h) : A (g + h)
• has_option {g g' : G} (h1 : A g) (h2 : IsOption g' g) : A g'
• neg_of {g : G} (h1 : A g) : A (-g)
• closed_dicotic (B C : Set G) [Small.{u, u + 1} ↑B] [Small.{u, u + 1} ↑C] (hB : ∀ b ∈ B, A b) (hC : ∀ c ∈ C, A c) : B.Nonempty → C.Nonempty → Form.IsShort !{B | C} → A !{B | C}
• zero_mem : A 0
• isAmbient_of_mem {g : G} : A g → Form.IsShort g

instance MisereGames.instLongUniverseIsLong {G : Type (u + 1)} [Form G] : LongUniverse Form.IsLong

instance MisereGames.instShortUniverseIsShort {G : Type (u + 1)} [Form G] : ShortUniverse Form.IsShort

theorem MisereGames.Universe.sInf_closed {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {S : Set ↑(Set.Iic IsAmbient)} (hS : ∀ A ∈ S, Universe IsAmbient ↑A) : Universe IsAmbient ↑(sInf S)

An intersection of universes is a universe.

@[reducible, inline]

noncomputable abbrev MisereGames.Universe.closureOperator {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] : ClosureOperator ↑(Set.Iic IsAmbient)

The closure operator for finding the universal closure of a given set (in the context of a given ambient). Sends a bounded predicate to the smallest Universe IsAmbient containing it.

Equations

• MisereGames.Universe.closureOperator IsAmbient = ClosureOperator.ofCompletePred (fun (A : ↑(Set.Iic IsAmbient)) => MisereGames.Universe IsAmbient ↑A) ⋯

@[reducible, inline]

noncomputable abbrev MisereGames.Universe.closureBounded {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] (A : ↑(Set.Iic IsAmbient)) : ↑(Set.Iic IsAmbient)

The universal closure of a given set (within the context of a given ambient).

Equations

• MisereGames.Universe.closureBounded IsAmbient A = (MisereGames.Universe.closureOperator IsAmbient) A

@[reducible, inline]

noncomputable abbrev MisereGames.Universe.closure {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] (A : G → Prop) (hA : A ≤ IsAmbient) : G → Prop

The universal closure of a given set (within the context of a given ambient).

Equations

• MisereGames.Universe.closure IsAmbient A hA = ↑(MisereGames.Universe.closureBounded IsAmbient ⟨A, hA⟩)

theorem MisereGames.Universe.subset_closure {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A : G → Prop} (hA : A ≤ IsAmbient) : A ≤ closure IsAmbient A hA

theorem MisereGames.Universe.mem_closure_of_mem {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A : G → Prop} {g : G} (hA : A ≤ IsAmbient) (hg : A g) : closure IsAmbient A hA g

theorem MisereGames.Universe.closure_le_ambient {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A : G → Prop} (hA : A ≤ IsAmbient) : closure IsAmbient A hA ≤ IsAmbient

instance MisereGames.Universe.closure_universe {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A : G → Prop} (hA : A ≤ IsAmbient) : Universe IsAmbient (closure IsAmbient A hA)

theorem MisereGames.Universe.closure_min {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A B : G → Prop} (hA : A ≤ IsAmbient) (hAB : A ≤ B) [Universe IsAmbient B] : closure IsAmbient A hA ≤ B

theorem MisereGames.Universe.closure_le {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A B : G → Prop} (hA : A ≤ IsAmbient) [Universe IsAmbient B] : closure IsAmbient A hA ≤ B ↔ A ≤ B

theorem MisereGames.Universe.closure_mono {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A B : G → Prop} {hA : A ≤ IsAmbient} {hB : B ≤ IsAmbient} (hAB : A ≤ B) : closure IsAmbient A hA ≤ closure IsAmbient B hB

theorem MisereGames.Universe.iInter {G : Type (u + 1)} [Form G] {ι : Sort u_1} (IsAmbient A : ι → G → Prop) [∀ (i : ι), Universe (IsAmbient i) (A i)] : Universe (fun (g : G) => ∀ (i : ι), IsAmbient i g) fun (g : G) => ∀ (i : ι), A i g

The intersection of universes is a universe, with ambient space the intersection of the ambient spaces.

theorem MisereGames.Universe.iUnion_of_directed {G : Type (u + 1)} [Form G] {ι : Sort u_1} [Nonempty ι] (IsAmbient A : ι → G → Prop) [∀ (i : ι), Universe (IsAmbient i) (A i)] (h_directed : Directed (fun (P Q : (G → Prop) × (G → Prop)) => P.1 ≤ Q.1 ∧ P.2 ≤ Q.2) fun (i : ι) => (A i, IsAmbient i)) (h_options : ∀ (B C : Set G) [inst : Small.{u, u + 1} ↑B] [inst_1 : Small.{u, u + 1} ↑C], (∀ b ∈ B, ∃ (i : ι), A i b) → (∀ c ∈ C, ∃ (i : ι), A i c) → B.Nonempty → C.Nonempty → (∃ (i : ι), IsAmbient i !{B | C}) → ∃ (i : ι), (∀ b ∈ B, A i b) ∧ (∀ c ∈ C, A i c) ∧ IsAmbient i !{B | C}) : Universe (fun (g : G) => ∃ (i : ι), IsAmbient i g) fun (g : G) => ∃ (i : ι), A i g

The union of a nonempty directed family of universes is a universe, with ambient space the union of the ambient spaces.

The directedness is componentwise on the family of ordered pairs (A i, IsAmbient i). We require the hypothesis that, if the Left and Right options lie in the union, and the form from dicotic closure lies in the union of the ambient spaces, then there exists a universe containing all of the options, and whose ambient space contains the relevant form. This extra hypothesis supplies the common index needed for dicotic closure.

theorem MisereGames.Universe.iUnion_of_directed_of_fixed_ambient {G : Type (u + 1)} [Form G] {ι : Sort u_1} [Nonempty ι] (IsAmbient : G → Prop) (A : ι → G → Prop) [∀ (i : ι), Universe IsAmbient (A i)] (h_directed : Directed (fun (x1 x2 : G → Prop) => x1 ≤ x2) A) (h_options : ∀ (B C : Set G) [inst : Small.{u, u + 1} ↑B] [inst_1 : Small.{u, u + 1} ↑C], (∀ b ∈ B, ∃ (i : ι), A i b) → (∀ c ∈ C, ∃ (i : ι), A i c) → B.Nonempty → C.Nonempty → IsAmbient !{B | C} → ∃ (i : ι), (∀ b ∈ B, A i b) ∧ ∀ c ∈ C, A i c) : Universe IsAmbient fun (g : G) => ∃ (i : ι), A i g

A specialised version of Universe.iUnion_of_directed in which every universe has the same ambient space.

@[reducible, inline]

noncomputable abbrev MisereGames.LongUniverse.closure {G : Type (u + 1)} [Form G] (A : G → Prop) : G → Prop

The smallest long universe containing A.

Equations

• MisereGames.LongUniverse.closure A = MisereGames.Universe.closure MisereGames.Form.IsLong A ⋯

instance MisereGames.LongUniverse.closure_universe {G : Type (u + 1)} [Form G] (A : G → Prop) : LongUniverse (closure A)

theorem MisereGames.LongUniverse.closure_le {G : Type (u + 1)} [Form G] {A B : G → Prop} [LongUniverse B] : closure A ≤ B ↔ A ≤ B

@[reducible, inline]

noncomputable abbrev MisereGames.ShortUniverse.closure {G : Type (u + 1)} [Form G] (A : G → Prop) (hA : A ≤ Form.IsShort) : G → Prop

The smallest short universe containing A.

Equations

• MisereGames.ShortUniverse.closure A hA = MisereGames.Universe.closure MisereGames.Form.IsShort A hA

instance MisereGames.ShortUniverse.closure_universe {G : Type (u + 1)} [Form G] {A : G → Prop} (hA : A ≤ Form.IsShort) : ShortUniverse (closure A hA)

theorem MisereGames.ShortUniverse.closure_le {G : Type (u + 1)} [Form G] {A B : G → Prop} (hA : A ≤ Form.IsShort) [ShortUniverse B] : closure A hA ≤ B ↔ A ≤ B

theorem MisereGames.ShortUniverse.iUnion_of_directed {G : Type (u + 1)} [Form G] {ι : Sort u_1} [Nonempty ι] (A : ι → G → Prop) [∀ (i : ι), ShortUniverse (A i)] (h_directed : Directed (fun (x1 x2 : G → Prop) => x1 ≤ x2) A) : ShortUniverse fun (g : G) => ∃ (i : ι), A i g

The union of a nonempty directed family of short universes is a short universe.