Misere combinatorial games.

Preservation of closure properties

There are some preservation properties between the closure operators of CombinatorialGames.Misere.Closures: for example, the hereditary closure of a conjugate closed set is still conjugate closed. In particular, the four closure properties can be chained together to obtain a universe (closureChain_universe), and this chain in fact computes the universal closure (closureChain_eq_universeClosure).

The closures preservations

instance MisereGames.Form.Misere.Preservation.hereditaryClosure_closedUnderNeg {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderNeg A] : ClosedUnderNeg (Hereditary.closure A)

The hereditary closure of a conjugate closed set is conjugate closed.

instance MisereGames.Form.Misere.Preservation.closedUnderNegClosure_hereditary {G : Type (u + 1)} [Form G] {A : G → Prop} [Hereditary A] : Hereditary (ClosedUnderNeg.closure A)

The conjugate closure of a hereditary set is hereditary.

theorem MisereGames.Form.Misere.Preservation.closedUnderNegClosure_hereditaryClosure_comm {G : Type (u + 1)} [Form G] (A : G → Prop) : ClosedUnderNeg.closure (Hereditary.closure A) = Hereditary.closure (ClosedUnderNeg.closure A)

Conjugate closure commutes with hereditary closure.

instance MisereGames.Form.Misere.Preservation.closedUnderSumClosure_hereditary {G : Type (u + 1)} [Form G] {A : G → Prop} [Hereditary A] : Hereditary (ClosedUnderAdd.closure A)

The additive closure of a hereditary set is hereditary.

instance MisereGames.Form.Misere.Preservation.closedUnderSumClosure_closedUnderNeg {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderNeg A] : ClosedUnderNeg (ClosedUnderAdd.closure A)

The additive closure of a conjugate closed set is conjugate closed.

instance MisereGames.Form.Misere.Preservation.closedUnderDicoticClosure_hereditary {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Hereditary A] : Hereditary (ClosedUnderDicotic.closure IsAmbient A)

The dicotic closure of a hereditary set is hereditary.

instance MisereGames.Form.Misere.Preservation.closedUnderDicoticClosure_closedUnderNeg {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [ClosedUnderNeg IsAmbient] [ClosedUnderNeg A] : ClosedUnderNeg (ClosedUnderDicotic.closure IsAmbient A)

The dicotic closure of a conjugate closed set is conjugate closed (when the ambient set is conjugate closed).

Dicotic closure preserves addition

This is slightly delicate: a sum need not be dicotic, so we consider cases where it is end-like and recurse on options otherwise.

theorem MisereGames.Form.Misere.Preservation.closedUnderDicoticClosure_closedUnderSum {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [ClosedUnderAdd IsAmbient] [ClosedUnderAdd A] [Hereditary A] (hA : A ≤ IsAmbient) : ClosedUnderAdd (ClosedUnderDicotic.closure IsAmbient A)

The dicotic closure of an additively closed hereditary set is additively closed.

The closure chain

@[reducible, inline]

noncomputable abbrev MisereGames.Form.Misere.Preservation.closureChain {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : G → Prop

The set obtained by applying the conjugate, hereditary, additive, and dicotic closures in that order.

Equations

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

theorem MisereGames.Form.Misere.Preservation.closureChain_universe {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Universe IsAmbient IsAmbient] (hA : A ≤ IsAmbient) (h0 : A 0) : Universe IsAmbient (closureChain IsAmbient A)

The conjugate–hereditary–additive–dicotic closure chain yields a universe.

theorem MisereGames.Form.Misere.Preservation.closureChain_eq_universeClosure {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Universe IsAmbient IsAmbient] (hA : A ≤ IsAmbient) (h0 : A 0) : closureChain IsAmbient A = Universe.closure IsAmbient A hA

The closure chain agrees with the universal closure operator.

theorem MisereGames.Form.Misere.Preservation.closureChain_longUniverse {G : Type (u + 1)} [Form G] {A : G → Prop} (h0 : A 0) : LongUniverse (closureChain IsLong A)

The conjugate–hereditary–additive–dicotic closure chain yields a long universe.

theorem MisereGames.Form.Misere.Preservation.closureChain_eq_longUniverseClosure {G : Type (u + 1)} [Form G] {A : G → Prop} (h0 : A 0) : closureChain IsLong A = LongUniverse.closure A

The long closure chain agrees with the long universal closure operator.

theorem MisereGames.Form.Misere.Preservation.closureChain_shortUniverse {G : Type (u + 1)} [Form G] {A : G → Prop} (hA : A ≤ IsShort) (h0 : A 0) : ShortUniverse (closureChain IsShort A)

The conjugate–hereditary–additive–dicotic closure chain yields a short universe.

theorem MisereGames.Form.Misere.Preservation.closureChain_eq_shortUniverseClosure {G : Type (u + 1)} [Form G] {A : G → Prop} (hA : A ≤ IsShort) (h0 : A 0) : closureChain IsShort A = ShortUniverse.closure A hA

The short closure chain agrees with the short universal closure operator.

Seed correspondence

A universe is recovered from its p end-like positions: the universal closure gives a bijection between the bounded p seeds and the universes within a fixed ambient set.

def MisereGames.Form.Misere.Preservation.endLikePart {G : Type (u + 1)} [Form G] (p : Player) (A : G → Prop) : G → Prop

The p end-like part of a set of games.

Equations

• MisereGames.Form.Misere.Preservation.endLikePart p A g = (A g ∧ MisereGames.Form.IsEndLike p g)

theorem MisereGames.Form.Misere.Preservation.endLikePart_le {G : Type (u + 1)} [Form G] (p : Player) (A : G → Prop) : endLikePart p A ≤ A

theorem MisereGames.Form.Misere.Preservation.endLikePart_le_ambient {G : Type (u + 1)} [Form G] (p : Player) {IsAmbient A : G → Prop} [Universe IsAmbient A] : endLikePart p A ≤ IsAmbient

class MisereGames.Form.Misere.Preservation.EndLikeClosed {G : Type (u + 1)} [Form G] (p : Player) (A : G → Prop) : Prop

A set of games closed under taking relevant end-like subpositions for player p.

• neg_mem_of_isEndLike_neg {g : G} (hg : A g) (hEnd : IsEndLike (-p) g) : A (-g)
• mem_of_subposition_isEndLike {g h : G} (hg : A g) (hsub : Subposition h g) (hEnd : IsEndLike p h) : A h
• neg_mem_of_subposition_isEndLike_neg {g h : G} (hg : A g) (hsub : Subposition h g) (hEnd : IsEndLike (-p) h) : A (-h)

class MisereGames.Form.Misere.Preservation.EndLikeSeed {G : Type (u + 1)} [Form G] (p : Player) (A : G → Prop) extends MisereGames.Form.Misere.Preservation.EndLikeClosed p A, MisereGames.Form.ClosedUnderAdd A : Prop

A p seed: an additive set of p end-like games containing zero and its relevant end-like subpositions.

• neg_mem_of_isEndLike_neg {g : G} (hg : A g) (hEnd : IsEndLike (-p) g) : A (-g)
• mem_of_subposition_isEndLike {g h : G} (hg : A g) (hsub : Subposition h g) (hEnd : IsEndLike p h) : A h
• neg_mem_of_subposition_isEndLike_neg {g h : G} (hg : A g) (hsub : Subposition h g) (hEnd : IsEndLike (-p) h) : A (-h)
• has_add (g h : G) (h_g : A g) (h_h : A h) : A (g + h)
• zero_mem : A 0
• isEndLike_of_mem {g : G} : A g → IsEndLike p g

theorem MisereGames.Form.Misere.Preservation.endLikePart_universeClosure_eq_of_seed {G : Type (u + 1)} [Form G] {p : Player} {IsAmbient A : G → Prop} [Universe IsAmbient IsAmbient] [EndLikeSeed p A] (hA : A ≤ IsAmbient) : endLikePart p (Universe.closure IsAmbient A hA) = A

The p end-like part of the universe closure of a bounded p seed is the seed.

theorem MisereGames.Form.Misere.Preservation.endLikePart_seed_of_universe {G : Type (u + 1)} [Form G] {p : Player} {IsAmbient A : G → Prop} [Universe IsAmbient A] : EndLikeSeed p (endLikePart p A)

The p end-like part of a universe is a p seed.

theorem MisereGames.Form.Misere.Preservation.universeClosure_endLikePart_eq_of_universe {G : Type (u + 1)} [Form G] {p : Player} {IsAmbient A : G → Prop} [Universe IsAmbient IsAmbient] [Universe IsAmbient A] : Universe.closure IsAmbient (endLikePart p A) ⋯ = A

A universe is the universal closure of its p end-like part.

The seed–universe bijection

def MisereGames.Form.Misere.Preservation.AmbientEndLikeSeed (G : Type (u + 1)) [Form G] (IsAmbient : G → Prop) (p : Player) : Type (u + 1)

The type of p seeds contained in an ambient set.

Equations

• MisereGames.Form.Misere.Preservation.AmbientEndLikeSeed G IsAmbient p = { A : G → Prop // MisereGames.Form.Misere.Preservation.EndLikeSeed p A ∧ A ≤ IsAmbient }

def MisereGames.Form.Misere.Preservation.AmbientUniverse (G : Type (u + 1)) [Form G] (IsAmbient : G → Prop) : Type (u + 1)

The type of universes with a fixed ambient set.

Equations

• MisereGames.Form.Misere.Preservation.AmbientUniverse G IsAmbient = { A : G → Prop // MisereGames.Universe IsAmbient A }

noncomputable def MisereGames.Form.Misere.Preservation.endLikeSeedToUniverse (G : Type (u + 1)) [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] (p : Player) : AmbientEndLikeSeed G IsAmbient p → AmbientUniverse G IsAmbient

Sending a bounded p seed to its universe closure.

Equations

• MisereGames.Form.Misere.Preservation.endLikeSeedToUniverse G IsAmbient p A = ⟨MisereGames.Universe.closure IsAmbient ↑A ⋯, ⋯⟩

noncomputable def MisereGames.Form.Misere.Preservation.universeToEndLikeSeed (G : Type (u + 1)) [Form G] (IsAmbient : G → Prop) (p : Player) : AmbientUniverse G IsAmbient → AmbientEndLikeSeed G IsAmbient p

Sending a universe to its p end-like part.

Equations

• MisereGames.Form.Misere.Preservation.universeToEndLikeSeed G IsAmbient p A = ⟨MisereGames.Form.Misere.Preservation.endLikePart p ↑A, ⋯⟩

noncomputable def MisereGames.Form.Misere.Preservation.endLikeSeedEquivUniverse {G : Type (u + 1)} [Form G] {IsAmbient : G → Prop} [Universe IsAmbient IsAmbient] (p : Player) : AmbientEndLikeSeed G IsAmbient p ≃ AmbientUniverse G IsAmbient

Universe closure is an equivalence from bounded p seeds to universes, with inverse taking the p end-like part.

Equations

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

theorem MisereGames.Form.Misere.Preservation.endLikeSeedToUniverse_bijective {G : Type (u + 1)} [Form G] {IsAmbient : G → Prop} [Universe IsAmbient IsAmbient] (p : Player) : Function.Bijective (endLikeSeedToUniverse G IsAmbient p)

Universal closure gives a bijection from bounded p seeds to universes.

theorem MisereGames.Form.Misere.Preservation.endLikePart_longUniverseClosure_eq_of_seed {G : Type (u + 1)} [Form G] {p : Player} {A : G → Prop} [EndLikeSeed p A] : endLikePart p (LongUniverse.closure A) = A

The p end-like part of the long universal closure of a p seed is the seed.

theorem MisereGames.Form.Misere.Preservation.endLikePart_seed_of_longUniverse {G : Type (u + 1)} [Form G] {p : Player} {A : G → Prop} [LongUniverse A] : EndLikeSeed p (endLikePart p A)

The p end-like part of a long universe is a p seed.

theorem MisereGames.Form.Misere.Preservation.longUniverseClosure_endLikePart_eq_of_longUniverse {G : Type (u + 1)} [Form G] {p : Player} {A : G → Prop} [LongUniverse A] : LongUniverse.closure (endLikePart p A) = A

A long universe is the long universal closure of its p end-like part.

theorem MisereGames.Form.Misere.Preservation.endLikeSeedToLongUniverse_bijective {G : Type (u + 1)} [Form G] (p : Player) : Function.Bijective (endLikeSeedToUniverse G IsLong p)

Long universal closure gives a bijection from p seeds to long universes.

theorem MisereGames.Form.Misere.Preservation.endLikePart_shortUniverseClosure_eq_of_seed {G : Type (u + 1)} [Form G] {p : Player} {A : G → Prop} [EndLikeSeed p A] (hA : A ≤ IsShort) : endLikePart p (ShortUniverse.closure A hA) = A

The p end-like part of the short universal closure of a short p seed is the seed.

theorem MisereGames.Form.Misere.Preservation.endLikePart_seed_of_shortUniverse {G : Type (u + 1)} [Form G] {p : Player} {A : G → Prop} [ShortUniverse A] : EndLikeSeed p (endLikePart p A)

The p end-like part of a short universe is a p seed.

theorem MisereGames.Form.Misere.Preservation.shortUniverseClosure_endLikePart_eq_of_shortUniverse {G : Type (u + 1)} [Form G] {p : Player} {A : G → Prop} [ShortUniverse A] : ShortUniverse.closure (endLikePart p A) ⋯ = A

A short universe is the short universal closure of its p end-like part.

theorem MisereGames.Form.Misere.Preservation.endLikeSeedToShortUniverse_bijective {G : Type (u + 1)} [Form G] (p : Player) : Function.Bijective (endLikeSeedToUniverse G IsShort p)

Short universal closure gives a bijection from short p seeds to short universes.