Documentation

TauCeti.AlgebraicGeometry.AdicSpace.FarguesFontaine.Window

Frobenius windows in 𝒴 = D(p) ∩ D([Ο–]) #

Give the Witt vectors π•Ž R the (p, [Ο–])-adic topology and let 𝒴 βŠ† Spa(π•Ž R, π•Ž R) be the open subset D(p) ∩ D([Ο–]) (TauCeti.FarguesFontaine.spaY). At a point v ∈ 𝒴 the radius ΞΊ(v) is the ratio log v([Ο–]) / log v(p). It is a real number only when v has rank one, so it is never formed here; instead, for a nonnegative rational q = a / b, the bounds

q ≀ ΞΊ(v)   :⇔   v([Ο–]) ^ b ≀ v(p) ^ a,
ΞΊ(v) ≀ q   :⇔   v(p) ^ a ≀ v([Ο–]) ^ b

are taken as definitions (IsRadiusLowerBound, IsRadiusUpperBound), and are independent of the chosen fraction. With the breakpoint c = (p + 1) / 2, which satisfies 1 < c < p, the Frobenius windows are, for every integer n,

U_n = {v ∈ 𝒴 : p ^ n ≀ ΞΊ(v) ≀ c p ^ n},
V_n = {v ∈ 𝒴 : c p ^ n ≀ ΞΊ(v) ≀ p ^ (n + 1)}.

They are rational subsets of Spa(π•Ž R, π•Ž R) and cover 𝒴. Since Frobenius multiplies the radius by p, pulling back along it carries U_n into U_(n+1) and V_n into V_(n+1), and different windows in one family are disjoint. Hence the Frobenius iterates act freely on 𝒴, and every window is wandering: it meets none of its Frobenius translates. These are the charts on which the adic Fargues–Fontaine curve 𝒴 / Ο†^β„€ is built.

Main definitions #

Main results #

References #

Radius bounds #

source
def TauCeti.FarguesFontaine.IsRadiusLowerBound (p : β„•) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (Ο– : R) (q : β„šβ‰₯0) (v : ValuationSpectrum (WittVector p R)) :
Prop

The lower radius bound q ≀ ΞΊ(v) at a point v of Spv (π•Ž R): writing q = a / b in lowest terms, v([Ο–]) ^ b ≀ v(p) ^ a. Here ΞΊ(v) stands for the ratio log v([Ο–]) / log v(p), which is not formed; isRadiusLowerBound_iff_of_eq_div reads the bound off any fraction.

Equations
Instances For
    source
    def TauCeti.FarguesFontaine.IsRadiusUpperBound (p : β„•) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (Ο– : R) (q : β„šβ‰₯0) (v : ValuationSpectrum (WittVector p R)) :
    Prop

    The upper radius bound ΞΊ(v) ≀ q at a point v of Spv (π•Ž R): writing q = a / b in lowest terms, v(p) ^ a ≀ v([Ο–]) ^ b. isRadiusUpperBound_iff_of_eq_div reads the bound off any fraction.

    Equations
    Instances For
      source
      theorem TauCeti.FarguesFontaine.isRadiusLowerBound_iff_of_eq_div {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} {q : β„šβ‰₯0} {a b : β„•} (hb : b β‰  0) (hq : q = ↑a / ↑b) (v : ValuationSpectrum (WittVector p R)) :
      IsRadiusLowerBound p Ο– q v ↔ (WittVector.teichmuller p) Ο– ^ b ≀α΅₯ ↑p ^ a

      The lower radius bound from any fraction: if q = a / b with b β‰  0, then q ≀ ΞΊ(v) exactly when v([Ο–]) ^ b ≀ v(p) ^ a.

      source
      theorem TauCeti.FarguesFontaine.isRadiusUpperBound_iff_of_eq_div {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} {q : β„šβ‰₯0} {a b : β„•} (hb : b β‰  0) (hq : q = ↑a / ↑b) (v : ValuationSpectrum (WittVector p R)) :
      IsRadiusUpperBound p Ο– q v ↔ ↑p ^ a ≀α΅₯ (WittVector.teichmuller p) Ο– ^ b

      The upper radius bound from any fraction: if q = a / b with b β‰  0, then ΞΊ(v) ≀ q exactly when v(p) ^ a ≀ v([Ο–]) ^ b.

      source
      theorem TauCeti.FarguesFontaine.isRadiusUpperBound_of_not_isRadiusLowerBound {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} {q : β„šβ‰₯0} {v : ValuationSpectrum (WittVector p R)} (h : Β¬IsRadiusLowerBound p Ο– q v) :
      IsRadiusUpperBound p Ο– q v

      A point that is not a lower bound q ≀ ΞΊ(v) satisfies the upper bound ΞΊ(v) ≀ q, since the value group is linearly ordered.

      source
      theorem TauCeti.FarguesFontaine.isRadiusLowerBound_comap_frobenius_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [CharP R p] (q : β„šβ‰₯0) (v : ValuationSpectrum (WittVector p R)) :
      IsRadiusLowerBound p Ο– q (ValuationSpectrum.comap WittVector.frobenius v) ↔ IsRadiusLowerBound p Ο– (q / ↑p) v

      Frobenius multiplies the radius by p, for lower bounds: q ≀ ΞΊ(Ο† v) exactly when q / p ≀ ΞΊ(v).

      source
      theorem TauCeti.FarguesFontaine.isRadiusUpperBound_comap_frobenius_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [CharP R p] (q : β„šβ‰₯0) (v : ValuationSpectrum (WittVector p R)) :
      IsRadiusUpperBound p Ο– q (ValuationSpectrum.comap WittVector.frobenius v) ↔ IsRadiusUpperBound p Ο– (q / ↑p) v

      Frobenius multiplies the radius by p, for upper bounds: ΞΊ(Ο† v) ≀ q exactly when ΞΊ(v) ≀ q / p.

      source
      theorem TauCeti.FarguesFontaine.IsRadiusLowerBound.of_le {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] {q q' : β„šβ‰₯0} {v : ValuationSpectrum (WittVector p R)} (hv : v ∈ ValuationSpectrum.spa ⊀) (h : IsRadiusLowerBound p Ο– q v) (hq : q' ≀ q) :
      IsRadiusLowerBound p Ο– q' v

      Lower radius bounds are closed downwards on Spa(π•Ž R, π•Ž R): if q ≀ ΞΊ(v) and q' ≀ q then q' ≀ ΞΊ(v), since v(p) ≀ 1.

      source
      theorem TauCeti.FarguesFontaine.IsRadiusUpperBound.of_le {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] {q q' : β„šβ‰₯0} {v : ValuationSpectrum (WittVector p R)} (hv : v ∈ ValuationSpectrum.spa ⊀) (h : IsRadiusUpperBound p Ο– q v) (hq : q ≀ q') :
      IsRadiusUpperBound p Ο– q' v

      Upper radius bounds are closed upwards on Spa(π•Ž R, π•Ž R): if ΞΊ(v) ≀ q and q ≀ q' then ΞΊ(v) ≀ q', since v(p) ≀ 1.

      source
      theorem TauCeti.FarguesFontaine.IsRadiusLowerBound.not_isRadiusUpperBound {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {q q' : β„šβ‰₯0} {v : ValuationSpectrum (WittVector p R)} (hv : v ∈ spaY p Ο–) (h : IsRadiusLowerBound p Ο– q v) (hq : q' < q) :
      Β¬IsRadiusUpperBound p Ο– q' v

      Separation of radius bounds on 𝒴: at a point of 𝒴 with q ≀ ΞΊ(v), no q' < q is an upper bound for ΞΊ(v). This uses 0 < v(p) < 1.

      source
      theorem TauCeti.FarguesFontaine.exists_isRadiusLowerBound_zpow {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {v : ValuationSpectrum (WittVector p R)} (hv : v ∈ spaY p Ο–) :
      βˆƒ (n : β„€), IsRadiusLowerBound p Ο– (↑p ^ n) v ∧ IsRadiusUpperBound p Ο– (↑p ^ (n + 1)) v

      The radius lies between consecutive powers of p: every point of 𝒴 satisfies p ^ n ≀ ΞΊ(v) ≀ p ^ (n + 1) for some integer n.

      The windows #

      source
      def TauCeti.FarguesFontaine.windowU (p : β„•) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] (Ο– : R) (n : β„€) :
      Set (ValuationSpectrum (WittVector p R))

      The window U_n = {v ∈ 𝒴 : p ^ n ≀ ΞΊ(v) ≀ c p ^ n}, with the breakpoint c = (p + 1) / 2.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def TauCeti.FarguesFontaine.windowV (p : β„•) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] (Ο– : R) (n : β„€) :
        Set (ValuationSpectrum (WittVector p R))

        The window V_n = {v ∈ 𝒴 : c p ^ n ≀ ΞΊ(v) ≀ p ^ (n + 1)}, with the breakpoint c = (p + 1) / 2.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem TauCeti.FarguesFontaine.mem_windowU_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (n : β„€) (v : ValuationSpectrum (WittVector p R)) :
          v ∈ windowU p Ο– n ↔ v ∈ spaY p Ο– ∧ IsRadiusLowerBound p Ο– (↑p ^ n) v ∧ IsRadiusUpperBound p Ο– ((↑p + 1) / 2 * ↑p ^ n) v

          Membership in U_n: a point of 𝒴 with p ^ n ≀ ΞΊ(v) ≀ c p ^ n.

          source
          @[simp]
          theorem TauCeti.FarguesFontaine.mem_windowV_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (n : β„€) (v : ValuationSpectrum (WittVector p R)) :
          v ∈ windowV p Ο– n ↔ v ∈ spaY p Ο– ∧ IsRadiusLowerBound p Ο– ((↑p + 1) / 2 * ↑p ^ n) v ∧ IsRadiusUpperBound p Ο– (↑p ^ (n + 1)) v

          Membership in V_n: a point of 𝒴 with c p ^ n ≀ ΞΊ(v) ≀ p ^ (n + 1).

          source
          theorem TauCeti.FarguesFontaine.windowU_subset_spaY {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (n : β„€) :
          windowU p Ο– n βŠ† spaY p Ο–

          U_n βŠ† 𝒴.

          source
          theorem TauCeti.FarguesFontaine.windowV_subset_spaY {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (n : β„€) :
          windowV p Ο– n βŠ† spaY p Ο–

          V_n βŠ† 𝒴.

          source
          theorem TauCeti.FarguesFontaine.iUnion_windowU_union_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) :
          ⋃ (n : β„€), windowU p Ο– n βˆͺ windowV p Ο– n = spaY p Ο–

          The windows cover 𝒴: every point of 𝒴 lies in some U_n or V_n.

          source
          theorem TauCeti.FarguesFontaine.val_preimage_windowU_mem_spaRationalFamily {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (Ο– : R) [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
          Subtype.val ⁻¹' windowU p Ο– n ∈ ValuationSpectrum.spaRationalFamily ⊀

          U_n is a rational subset of Spa(π•Ž R, π•Ž R), for the (p, [Ο–])-adic topology.

          source
          theorem TauCeti.FarguesFontaine.val_preimage_windowV_mem_spaRationalFamily {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (Ο– : R) [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
          Subtype.val ⁻¹' windowV p Ο– n ∈ ValuationSpectrum.spaRationalFamily ⊀

          V_n is a rational subset of Spa(π•Ž R, π•Ž R), for the (p, [Ο–])-adic topology.

          source
          theorem TauCeti.FarguesFontaine.isOpen_val_preimage_windowU {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
          IsOpen (Subtype.val ⁻¹' windowU p Ο– n)

          Each U window is open in 𝒴.

          source
          theorem TauCeti.FarguesFontaine.isOpen_val_preimage_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
          IsOpen (Subtype.val ⁻¹' windowV p Ο– n)

          Each V window is open in 𝒴.

          source
          theorem TauCeti.FarguesFontaine.isCompact_val_preimage_windowU {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
          IsCompact (Subtype.val ⁻¹' windowU p Ο– n)

          Each U window is quasi-compact as a subset of 𝒴.

          source
          theorem TauCeti.FarguesFontaine.isCompact_val_preimage_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
          IsCompact (Subtype.val ⁻¹' windowV p Ο– n)

          Each V window is quasi-compact as a subset of 𝒴.

          Frobenius on the windows #

          source
          theorem TauCeti.FarguesFontaine.disjoint_windowU {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {m n : β„€} (h : m β‰  n) :
          Disjoint (windowU p Ο– m) (windowU p Ο– n)

          Disjointness of the U windows: U_m ∩ U_n = βˆ… for m β‰  n, because c p ^ m < p ^ (m + 1).

          source
          theorem TauCeti.FarguesFontaine.disjoint_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {m n : β„€} (h : m β‰  n) :
          Disjoint (windowV p Ο– m) (windowV p Ο– n)

          Disjointness of the V windows: V_m ∩ V_n = βˆ… for m β‰  n, because p ^ (m + 1) < c p ^ (m + 1).

          source
          theorem TauCeti.FarguesFontaine.comap_frobenius_mem_windowU {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {v : ValuationSpectrum (WittVector p R)} {n : β„€} (hv : v ∈ windowU p Ο– n) :
          ValuationSpectrum.comap WittVector.frobenius v ∈ windowU p Ο– (n + 1)

          Frobenius shifts the U windows: pulling a point of U_n back along Frobenius gives a point of U_(n+1).

          source
          theorem TauCeti.FarguesFontaine.comap_frobenius_mem_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {v : ValuationSpectrum (WittVector p R)} {n : β„€} (hv : v ∈ windowV p Ο– n) :
          ValuationSpectrum.comap WittVector.frobenius v ∈ windowV p Ο– (n + 1)

          Frobenius shifts the V windows: pulling a point of V_n back along Frobenius gives a point of V_(n+1).

          source
          theorem TauCeti.FarguesFontaine.comap_frobenius_mem_windowU_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (v : ValuationSpectrum (WittVector p R)) (n : β„€) :
          ValuationSpectrum.comap WittVector.frobenius v ∈ windowU p Ο– (n + 1) ↔ v ∈ windowU p Ο– n

          Frobenius shifts the U windows exactly: for perfect R, a point lies in U_n exactly when its pullback along Frobenius lies in U_(n+1).

          source
          theorem TauCeti.FarguesFontaine.comap_frobenius_mem_windowV_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (v : ValuationSpectrum (WittVector p R)) (n : β„€) :
          ValuationSpectrum.comap WittVector.frobenius v ∈ windowV p Ο– (n + 1) ↔ v ∈ windowV p Ο– n

          Frobenius shifts the V windows exactly: for perfect R, a point lies in V_n exactly when its pullback along Frobenius lies in V_(n+1).

          source
          theorem TauCeti.FarguesFontaine.mapsTo_iterate_comap_frobenius_windowU {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) (k : β„•) :
          Set.MapsTo (ValuationSpectrum.comap WittVector.frobenius)^[k] (windowU p Ο– n) (windowU p Ο– (n + ↑k))

          Iterating Frobenius k times carries U_n into U_(n+k).

          source
          theorem TauCeti.FarguesFontaine.mapsTo_iterate_comap_frobenius_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) (k : β„•) :
          Set.MapsTo (ValuationSpectrum.comap WittVector.frobenius)^[k] (windowV p Ο– n) (windowV p Ο– (n + ↑k))

          Iterating Frobenius k times carries V_n into V_(n+k).

          source
          theorem TauCeti.FarguesFontaine.disjoint_image_iterate_comap_frobenius_windowU {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) {k : β„•} (hk : k β‰  0) :
          Disjoint ((ValuationSpectrum.comap WittVector.frobenius)^[k] '' windowU p Ο– n) (windowU p Ο– n)

          The U windows are wandering: a nontrivial Frobenius iterate moves U_n off itself.

          source
          theorem TauCeti.FarguesFontaine.disjoint_image_iterate_comap_frobenius_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) {k : β„•} (hk : k β‰  0) :
          Disjoint ((ValuationSpectrum.comap WittVector.frobenius)^[k] '' windowV p Ο– n) (windowV p Ο– n)

          The V windows are wandering: a nontrivial Frobenius iterate moves V_n off itself.

          source
          theorem TauCeti.FarguesFontaine.iterate_comap_frobenius_ne {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {v : ValuationSpectrum (WittVector p R)} (hv : v ∈ spaY p Ο–) {k : β„•} (hk : k β‰  0) :
          (ValuationSpectrum.comap WittVector.frobenius)^[k] v β‰  v

          Frobenius acts freely on 𝒴: no nontrivial Frobenius iterate fixes a point of 𝒴.

          source
          theorem TauCeti.FarguesFontaine.frobeniusHomeomorph_zpow_mem_windowU_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n m : β„€) (v : ↑(spaY p Ο–)) :
          ↑((frobeniusHomeomorph hI ^ n) v) ∈ windowU p Ο– (m + n) ↔ ↑v ∈ windowU p Ο– m

          An integer Frobenius translate shifts the index of a U window by that integer.

          source
          theorem TauCeti.FarguesFontaine.frobeniusHomeomorph_zpow_mem_windowV_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {Ο– : R} [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n m : β„€) (v : ↑(spaY p Ο–)) :
          ↑((frobeniusHomeomorph hI ^ n) v) ∈ windowV p Ο– (m + n) ↔ ↑v ∈ windowV p Ο– m

          An integer Frobenius translate shifts the index of a V window by that integer.