Grace/Cumulus/FixedPoint/KuhnLift.g17

Open in Workbench Download source

Imports

KuhnWallSimplex

Declarations

Source

1-- Lifting a Kuhn simplex of the lower cube to one whose far-wall face2-- restricts back to it: the base gains the value p − 1 at the last3-- coordinate and the permutation sends 0 there first4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.FixedPoint.KuhnLift10import KuhnWallSimplex1112def liftBase (m q b : Set) : Set := b ∪ constantFunction({m}, ℕ, q)1314def liftPerm (m u : Set) : Set := unrotated(succ(m), u ∪ constantFunction({m}, {m}, m))1516theorem successor.as_union (m : Nat)17  shows m ∪ {m} = succ(m)18proof19  have asInsert := natural.successor_as_insert at m20  have unfolded : insert(m, m) = {m} ∪ m21    unfold insert22    rfl23  rw [asInsert, unfolded]24  exact union2.commutative2526theorem liftBase.function (m q : Nat) (b : Set)27  requires baseFunction : b : m → ℕ28  shows liftBase(m, q, b) : succ(m) → ℕ29proof30  have qNat : Nat(q) by typecheck31  have qIn := nat.omega.forward with qNat32  have constant := constantFunction.function at {m}, ℕ, q with qIn33  have disjoint := cubeExtend.disjoint at m34  have union := FunctionBetween.union_disjoint with baseFunction, constant, disjoint35  have domain := successor.as_union at m36  have codomain := union2.idempotent at ℕ37  rw [domain, codomain] at union38  have same : liftBase(m, q, b) = b ∪ constantFunction({m}, ℕ, q)39    unfold liftBase40    rfl41  rwa same4243theorem liftBase.apply_below (m q : Nat) (b j : Set)44  requires baseFunction : b : m → ℕ45  requires hj : j ∈ m46  shows liftBase(m, q, b)(j) = b(j)47proof48  have qNat : Nat(q) by typecheck49  have qIn := nat.omega.forward with qNat50  have constant := constantFunction.function at {m}, ℕ, q with qIn51  have disjoint := cubeExtend.disjoint at m52  have same : liftBase(m, q, b) = b ∪ constantFunction({m}, ℕ, q)53    unfold liftBase54    rfl55  rw same56  exact FunctionBetween.union_apply_left with baseFunction, constant, disjoint, hj5758theorem liftBase.apply_top (m q : Nat) (b : Set)59  requires baseFunction : b : m → ℕ60  shows liftBase(m, q, b)(m) = q61proof62  have qNat : Nat(q) by typecheck63  have qIn := nat.omega.forward with qNat64  have constant := constantFunction.function at {m}, ℕ, q with qIn65  have disjoint := cubeExtend.disjoint at m66  have mIn : m ∈ {m}67    apply singleton.membership.backward68    rfl69  have same : liftBase(m, q, b) = b ∪ constantFunction({m}, ℕ, q)70    unfold liftBase71    rfl72  rw same73  have value := FunctionBetween.union_apply_right with baseFunction, constant, disjoint, mIn74  rw value75  exact constantFunction.apply with mIn, qIn7677theorem liftBase.restrict (m q : Nat) (b : Set)78  requires baseFunction : b : m → ℕ79  shows restrict(liftBase(m, q, b), m) = b80proof81  have lifted := liftBase.function at m, q, b with baseFunction82  have mSubset := successor.subset at m83  have restricted := restrict.domain_function with lifted, mSubset84  apply FunctionBetween.ext with restricted, baseFunction85  intros j hj86  have value := restrict.domain_apply with lifted, mSubset, hj87  rw value88  exact liftBase.apply_below with baseFunction, hj8990theorem constantFunction.bijective_singleton (a : Set)91  shows BijectiveBetween(constantFunction({a}, {a}, a), {a}, {a})92proof93  have aIn : a ∈ {a}94    apply singleton.membership.backward95    rfl96  have function := constantFunction.function at {a}, {a}, a with aIn97  constructor98  . apply Injective.of_cancel with function99    intros x hx y hy same100    have xEq := singleton.membership.forward with hx101    have yEq := singleton.membership.forward with hy102    rw [xEq, yEq]103    rfl104  . constructor105    . exact function106    . intros y hy107      have yEq := singleton.membership.forward with hy108      witness a109      constructor110      . exact aIn111      . have edge := FunctionBetween.relates_apply with function, aIn112        have value := constantFunction.apply with aIn, aIn113        rw value at edge114        rwa yEq115116theorem liftPerm.union_bijective (m : Nat) (u : Set)117  requires updBijective : BijectiveBetween(u, m, m)118  shows BijectiveBetween(u ∪ constantFunction({m}, {m}, m), succ(m), succ(m))119proof120  have single := constantFunction.bijective_singleton at m121  have disjoint := cubeExtend.disjoint at m122  have union := Bijective.union_disjoint with updBijective, single, disjoint, disjoint123  have domain := successor.as_union at m124  rwa domain at union125126theorem liftPerm.bijective (m : Nat) (u : Set)127  requires updBijective : BijectiveBetween(u, m, m)128  shows BijectiveBetween(liftPerm(m, u), succ(m), succ(m))129proof130  have union := liftPerm.union_bijective with updBijective131  have same : liftPerm(m, u) = unrotated(succ(m), u ∪ constantFunction({m}, {m}, m))132    unfold liftPerm133    rfl134  rw same135  exact unrotated.bijective with union136137theorem liftPerm.zero (m : Nat) (u : Set)138  requires updBijective : BijectiveBetween(u, m, m)139  shows liftPerm(m, u)(0) = m140proof141  have union := liftPerm.union_bijective with updBijective142  have uFunction := Injective.function with (Bijective.injective with updBijective)143  have mIn : m ∈ {m}144    apply singleton.membership.backward145    rfl146  have constant := constantFunction.function at {m}, {m}, m with mIn147  have disjoint := cubeExtend.disjoint at m148  have mInSucc := bootstrap.succ.self at m149  have top : succ(m) = succ(m) by rfl150  have same : liftPerm(m, u) = unrotated(succ(m), u ∪ constantFunction({m}, {m}, m))151    unfold liftPerm152    rfl153  rw same154  have wrap := unrotated.wrap with union, mInSucc, top155  rw wrap156  have value := FunctionBetween.union_apply_right with uFunction, constant, disjoint, mIn157  rw value158  exact constantFunction.apply with mIn, mIn159160theorem liftPerm.step (m : Nat) (u l : Set)161  requires updBijective : BijectiveBetween(u, m, m)162  requires hl : l ∈ m163  shows liftPerm(m, u)(succ(l)) = u(l)164proof165  have union := liftPerm.union_bijective with updBijective166  have uFunction := Injective.function with (Bijective.injective with updBijective)167  have mIn : m ∈ {m}168    apply singleton.membership.backward169    rfl170  have constant := constantFunction.function at {m}, {m}, m with mIn171  have disjoint := cubeExtend.disjoint at m172  have lIn := membership.into_successor with hl173  have lNat := natural.member at m with hl174  have lLess := Less.of_membership with hl175  have sLess : succ(l) < succ(m) by arith176  have sIn := membership.of_Less with sLess177  have same : liftPerm(m, u) = unrotated(succ(m), u ∪ constantFunction({m}, {m}, m))178    unfold liftPerm179    rfl180  rw same181  have step := unrotated.step with union, lIn, sIn182  rw step183  exact FunctionBetween.union_apply_left with uFunction, constant, disjoint, hl184185theorem wallPerm.lift (m : Nat) (u : Set)186  requires updBijective : BijectiveBetween(u, m, m)187  shows wallPerm(m, liftPerm(m, u)) = u188proof189  have lifted := liftPerm.bijective with updBijective190  have zero := liftPerm.zero with updBijective191  have wallBijective := wallPerm.bijective with lifted, zero192  have wallFunction := Injective.function with (Bijective.injective with wallBijective)193  have uFunction := Injective.function with (Bijective.injective with updBijective)194  apply FunctionBetween.ext with wallFunction, uFunction195  intros l hl196  have value := wallPerm.value with lifted, hl197  rw value198  exact liftPerm.step with updBijective, hl199200theorem kuhnSimplex.lift_in_family (m q : Nat) (b u : Set)201  requires baseFunction : b : m → ℕ202  requires bounds : ∀ j ∈ m, b(j) < succ(q)203  requires updBijective : BijectiveBetween(u, m, m)204  shows kuhnSimplex(succ(m), liftBase(m, q, b), liftPerm(m, u)) ∈ kuhnSimplices(succ(q), succ(m))205proof206  have liftFunction := liftBase.function at m, q, b with baseFunction207  have lifted := liftPerm.bijective with updBijective208  have liftBounds : ∀ j ∈ succ(m), liftBase(m, q, b)(j) < succ(q)209    intros j hj210    have split := bootstrap.succ.membership.forward with hj211    cases split with below | same212    . have value := liftBase.apply_below at m, q, b, j with baseFunction, below213      rw value214      exact bounds with below215    . rw same216      have value := liftBase.apply_top at m, q, b with baseFunction217      rw value218      arith219  exact kuhnSimplex.in_family with liftFunction, lifted, liftBounds220221-- Every vertex but the bottom of the lifted simplex lies on the far wall.222theorem kuhnSimplex.lift_top_wall (m q : Nat) (b u x : Set)223  requires baseFunction : b : m → ℕ224  requires updBijective : BijectiveBetween(u, m, m)225  requires hx : x ∈ kuhnSimplex(succ(m), liftBase(m, q, b), liftPerm(m, u)) ∖226    {kuhnVertex(succ(m), liftBase(m, q, b), liftPerm(m, u))(0)}227  shows x(m) = succ(q)228proof229  have liftFunction := liftBase.function at m, q, b with baseFunction230  have mIn := bootstrap.succ.self at m231  have parts := difference.singleton_membership.forward with hx232  obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with parts.left233  have iNat := natural.member at succ(succ(m)) with hi234  have zeroInI : 0 ∈ i235    have split := natural.zero_or_successor with iNat236    cases split with zero | successor237    . exfalso238      apply parts.right239      rw [shape, zero]240      rfl241    . obtain ⟨k, kNat, iEq⟩ := successor242      rw iEq243      have less : 0 < succ(k) by arith244      exact membership.of_Less with less245  have zero := liftPerm.zero with updBijective246  have raisedM : m ∈ raised(succ(m), liftPerm(m, u), i)247    apply raised.membership.backward248    constructor249    . exact mIn250    . witness 0251      constructor252      . exact zeroInI253      . symm254        exact zero255  have coordinate := kuhnVertex.coordinate at succ(m), liftBase(m, q, b), liftPerm(m, u), i, m with liftFunction, hi, mIn256  have one := indicator.member with raisedM257  have top := liftBase.apply_top at m, q, b with baseFunction258  rw [shape, coordinate, one, top]259  exact add.right_one260