Grace/Cumulus/FixedPoint/KuhnWallCount.g17

Open in Workbench Download source

Imports

KuhnLift

Declarations

Source

1-- Restricting far-wall faces to the lower cube is a bijection onto the2-- completely labelled simplices there, so the two counts agree3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.FixedPoint.KuhnWallCount9import KuhnLift1011defgraph wallRestrict (p m lab : Set) (f ∈ topWallFaces(p, m, lab)) : 𝒫(functionSpace(m, succ(p))) :=12  functionImage(cubeRestrict(m, p), f, functionSpace(m, succ(p)))13proof14  exact powerset.membership_iff.backward with (functionImage.subset at cubeRestrict(m, p), f, functionSpace(m, succ(p)))1516theorem topWallFaces.cube (m p : Nat) (lab f : Set)17  requires hf : f ∈ topWallFaces(p, m, lab)18  shows f ⊆ functionSpace(succ(m), succ(p)) ∧ ∀ x ∈ f, x(m) = p19proof20  obtain ⟨fIn, top⟩ := topWallFaces.membership.forward with hf21  have parts := labelledFaces.membership.forward with fIn22  constructor23  . exact powerset.membership_iff.forward with parts.left24  . exact top2526theorem wallRestrict.subset_of_image (m p : Nat) (f g : Set)27  requires fCube : f ⊆ functionSpace(succ(m), succ(p))28  requires fTop : ∀ x ∈ f, x(m) = p29  requires gCube : g ⊆ functionSpace(succ(m), succ(p))30  requires gTop : ∀ x ∈ g, x(m) = p31  requires inclusion : functionImage(cubeRestrict(m, p), f, functionSpace(m, succ(p))) ⊆32    functionImage(cubeRestrict(m, p), g, functionSpace(m, succ(p)))33  shows f ⊆ g34proof35  have function := cubeRestrict.function at m, p with *36  intros x hx37  have xIn := fCube with x, hx38  have value := cubeRestrict.value with xIn39  have inImage : cubeRestrict(m, p)(x) ∈ functionImage(cubeRestrict(m, p), f, functionSpace(m, succ(p)))40    apply functionImage.membership.backward41    constructor42    . exact FunctionBetween.apply_closed with function, xIn43    . witness x44      constructor45      . exact hx46      . rfl47  have inG := inclusion with inImage48  obtain ⟨yIn, x2, hx2, shape⟩ := functionImage.membership.forward with inG49  have x2In := gCube with x2, hx250  have value2 := cubeRestrict.value with x2In51  rw [value, value2] at shape52  have back := cubeRestrict.extend with xIn, (fTop with hx)53  have back2 := cubeRestrict.extend with x2In, (gTop with hx2)54  rwa [← back, shape, back2]5556theorem wallRestrict.injective (m p : Nat) (lab : Set)57  shows InjectiveBetween(wallRestrict(p, m, lab), topWallFaces(p, m, lab), 𝒫(functionSpace(m, succ(p))))58proof59  have function := wallRestrict.function at p, m, lab60  apply Injective.of_cancel with function61  intros f hf g hg same62  have fValue := wallRestrict.value with hf63  have gValue := wallRestrict.value with hg64  rw [fValue, gValue] at same65  obtain ⟨fCube, fTop⟩ := topWallFaces.cube with hf66  obtain ⟨gCube, gTop⟩ := topWallFaces.cube with hg67  have forward : functionImage(cubeRestrict(m, p), f, functionSpace(m, succ(p))) ⊆ functionImage(cubeRestrict(m, p), g, functionSpace(m, succ(p)))68    rw same69    intros y hy70    exact hy71  have backward : functionImage(cubeRestrict(m, p), g, functionSpace(m, succ(p))) ⊆ functionImage(cubeRestrict(m, p), f, functionSpace(m, succ(p)))72    rw same73    intros y hy74    exact hy75  apply Subset.antisymmetric76  . exact wallRestrict.subset_of_image with fCube, fTop, gCube, gTop, forward77  . exact wallRestrict.subset_of_image with gCube, gTop, fCube, fTop, backward7879-- The restriction of a far-wall face is a completely labelled simplex of the80-- lower cube.81theorem wallRestrict.complete (m p : Nat) (lab L f : Set)82  requires labFunction : lab : functionSpace(succ(m), succ(p)) → L83  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = p → lab(x)(j) = 184  requires hf : f ∈ topWallFaces(p, m, lab)85  shows wallRestrict(p, m, lab)(f) ∈ completeSimplices(p, m, wallLabels(m, p, lab, L))86proof87  have value := wallRestrict.value with hf88  rw value89  obtain ⟨fIn, top⟩ := topWallFaces.membership.forward with hf90  have fParts := labelledFaces.membership.forward with fIn91  have fCube := powerset.membership_iff.forward with fParts.left92  obtain ⟨s, hs, a, ha, shape⟩ := fParts.right.left93  have labels := fParts.right.right94  obtain ⟨b, baseFunction, bounds, u, updBijective, sShape⟩ := kuhnSimplices.shape with hs95  have updInjective := Bijective.injective with updBijective96  rw sShape at ha97  rw sShape at shape98  have mIn := bootstrap.succ.self at m99  have zeroLess : 0 < succ(m) by arith100  have positive := membership.of_Less with zeroLess101  have zeroLess2 : 0 < succ(succ(m)) by arith102  have zeroIn := membership.of_Less with zeroLess2103  obtain ⟨inSpace, i, hi, aShape⟩ := kuhnSimplex.membership.forward with ha104  have flat : ∀ x ∈ kuhnSimplex(succ(m), b, u) ∖ {kuhnVertex(succ(m), b, u)(i)}, x(m) = p105    rw under ← aShape106    rwa under ← shape107  have below := bounds with mIn108  have bottom := kuhnSimplex.full_face_bottom with baseFunction, updBijective, hi, mIn, below, flat109  rw bottom at aShape110  rw aShape at shape111  have oneLess : succ(0) < succ(succ(m)) by arith112  have oneIn := membership.of_Less with oneLess113  have oneMember := kuhnVertex.member at succ(m), b, u, succ(0) with baseFunction, oneIn114  have oneInFace : kuhnVertex(succ(m), b, u)(succ(0)) ∈ kuhnSimplex(succ(m), b, u) ∖ {kuhnVertex(succ(m), b, u)(0)}115    apply difference.singleton_membership.backward116    constructor117    . exact oneMember118    . intro equal119      have same := kuhnVertex.injective with baseFunction, updInjective, oneIn, zeroIn, equal120      arith121  rw ← shape at oneInFace122  have oneTop := top with oneInFace123  have first : u(0) = m124    have coordinate := kuhnVertex.coordinate_succ with baseFunction, updInjective, positive, mIn125    have zeroValue := kuhnVertex.zero_coordinate at succ(m), b, u, m with baseFunction, mIn126    rw [coordinate, zeroValue] at oneTop127    have baseNat := nat.omega.backward with (FunctionBetween.apply_closed with baseFunction, mIn)128    by_contra different129    have zero := indicator.singleton_other with different130    rw zero at oneTop131    arith132  have face := kuhnSimplex.wall_face with baseFunction, bounds, updBijective, first133  have imageEq : functionImage(cubeRestrict(m, p), f, functionSpace(m, succ(p))) =134      kuhnSimplex(m, restrict(b, m), wallPerm(m, u))135    rwa shape136  rw imageEq137  apply completeSimplices.membership.backward138  constructor139  . have mSubset := successor.subset at m140    have restrictedBase := restrict.domain_function with baseFunction, mSubset141    have restrictedBounds : ∀ j ∈ m, restrict(b, m)(j) < p142      intros j hj143      have baseValue := restrict.domain_apply with baseFunction, mSubset, hj144      rw baseValue145      exact bounds with (membership.into_successor with hj)146    have wallBijective := wallPerm.bijective with updBijective, first147    exact kuhnSimplex.in_family with restrictedBase, wallBijective, restrictedBounds148  . have transfer := labelImage.restrict_wall with labFunction, fullWall, fCube, top149    rwa [imageEq, labels] at transfer150151-- Every completely labelled simplex of the lower cube is the restriction of152-- a far-wall face.153theorem wallRestrict.onto (m q : Nat) (lab L t : Set)154  requires labFunction : lab : functionSpace(succ(m), succ(succ(q))) → L155  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(succ(q))), ∀ j ∈ succ(m), x(j) = succ(q) → lab(x)(j) = 1156  requires ht : t ∈ completeSimplices(succ(q), m, wallLabels(m, succ(q), lab, L))157  shows ∃ f ∈ topWallFaces(succ(q), m, lab), wallRestrict(succ(q), m, lab)(f) = t158proof159  obtain ⟨tIn, complete⟩ := completeSimplices.membership.forward with ht160  obtain ⟨b, baseFunction, bounds, u, updBijective, tShape⟩ := kuhnSimplices.shape with tIn161  have liftFunction := liftBase.function at m, q, b with baseFunction162  have lifted := liftPerm.bijective with updBijective163  have zero := liftPerm.zero with updBijective164  have liftBounds : ∀ j ∈ succ(m), liftBase(m, q, b)(j) < succ(q)165    intros j hj166    have split := bootstrap.succ.membership.forward with hj167    cases split with below | same168    . have value := liftBase.apply_below at m, q, b, j with baseFunction, below169      rw value170      exact bounds with below171    . rw same172      have value := liftBase.apply_top at m, q, b with baseFunction173      rw value174      arith175  have sIn := kuhnSimplex.lift_in_family with baseFunction, bounds, updBijective176  have face := kuhnSimplex.wall_face with liftFunction, liftBounds, lifted, zero177  have restrictBase := liftBase.restrict at m, q, b with baseFunction178  have restrictPerm := wallPerm.lift with updBijective179  rw [restrictBase, restrictPerm, ← tShape] at face180  have zeroLess : 0 < succ(succ(m)) by arith181  have zeroIn := membership.of_Less with zeroLess182  have bottomMember := kuhnVertex.member at succ(m), liftBase(m, q, b), liftPerm(m, u), 0 with liftFunction, zeroIn183  have faceCube : kuhnSimplex(succ(m), liftBase(m, q, b), liftPerm(m, u)) ∖ {kuhnVertex(succ(m), liftBase(m, q, b), liftPerm(m, u))(0)} ⊆ functionSpace(succ(m), succ(succ(q)))184    intros x hx185    have parts := difference.singleton_membership.forward with hx186    obtain ⟨inSpace, i, hi, xShape⟩ := kuhnSimplex.membership.forward with parts.left187    rw xShape188    exact kuhnVertex.into_cube with liftFunction, liftBounds, hi189  have faceTop : ∀ x ∈ kuhnSimplex(succ(m), liftBase(m, q, b), liftPerm(m, u)) ∖ {kuhnVertex(succ(m), liftBase(m, q, b), liftPerm(m, u))(0)}, x(m) = succ(q)190    intros x hx191    exact kuhnSimplex.lift_top_wall with baseFunction, updBijective, hx192  have faceIn : kuhnSimplex(succ(m), liftBase(m, q, b), liftPerm(m, u)) ∖ {kuhnVertex(succ(m), liftBase(m, q, b), liftPerm(m, u))(0)} ∈ topWallFaces(succ(q), m, lab)193    apply topWallFaces.membership.backward194    constructor195    . apply labelledFaces.membership.backward196      constructor197      . exact powerset.membership_iff.backward with faceCube198      . constructor199        . witness kuhnSimplex(succ(m), liftBase(m, q, b), liftPerm(m, u))200          constructor201          . exact sIn202          . witness kuhnVertex(succ(m), liftBase(m, q, b), liftPerm(m, u))(0)203            constructor204            . exact bottomMember205            . rfl206        . have transfer := labelImage.restrict_wall with labFunction, fullWall, faceCube, faceTop207          rw [face, complete] at transfer208          symm209          exact transfer210    . exact faceTop211  witness kuhnSimplex(succ(m), liftBase(m, q, b), liftPerm(m, u)) ∖ {kuhnVertex(succ(m), liftBase(m, q, b), liftPerm(m, u))(0)}212  constructor213  . exact faceIn214  . have value := wallRestrict.value at succ(q), m, lab, kuhnSimplex(succ(m), liftBase(m, q, b), liftPerm(m, u)) ∖ {kuhnVertex(succ(m), liftBase(m, q, b), liftPerm(m, u))(0)} with faceIn215    rwa value216217theorem topWallFaces.count (m q : Nat) (lab L : Set)218  requires labFunction : lab : functionSpace(succ(m), succ(succ(q))) → L219  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(succ(q))), ∀ j ∈ succ(m), x(j) = succ(q) → lab(x)(j) = 1220  shows cardinality(topWallFaces(succ(q), m, lab)) =221    cardinality(completeSimplices(succ(q), m, wallLabels(m, succ(q), lab, L)))222proof223  have injective := wallRestrict.injective at m, succ(q), lab224  have function := wallRestrict.function at succ(q), m, lab225  have selfSubset : topWallFaces(succ(q), m, lab) ⊆ topWallFaces(succ(q), m, lab)226    intros f hf227    exact hf228  have finite : Finite(topWallFaces(succ(q), m, lab))229    have inside : topWallFaces(succ(q), m, lab) ⊆ labelledFaces(succ(q), succ(m), lab)230      intros f hf231      have parts := topWallFaces.membership.forward with hf232      exact parts.left233    exact Finite.subset with (labelledFaces.finite at succ(m), succ(q), lab), inside234  have count := cardinality.injective_image with injective, selfSubset, finite235  have same : functionImage(wallRestrict(succ(q), m, lab), topWallFaces(succ(q), m, lab), 𝒫(functionSpace(m, succ(succ(q))))) =236      completeSimplices(succ(q), m, wallLabels(m, succ(q), lab, L))237    ext t238    constructor239    . intro ht240      obtain ⟨tIn, f, hf, shape⟩ := functionImage.membership.forward with ht241      rw shape242      exact wallRestrict.complete with labFunction, fullWall, hf243    . intro ht244      obtain ⟨f, hf, shape⟩ := wallRestrict.onto with labFunction, fullWall, ht245      apply functionImage.membership.backward246      constructor247      . rw ← shape248        exact FunctionBetween.apply_closed with function, hf249      . witness f250        constructor251        . exact hf252        . symm253          exact shape254  rw same at count255  symm256  exact count257