Sections and sectors of a stack

A finite family of functions θ₀ < θ₁ < … < θₖ₋₁ on a base X cuts the cylinder X × α into a stack: the k sections, which are the graphs of the θᵢ, and the k + 1 open sectors between consecutive graphs, the lowest and highest sectors being unbounded. These are the cells built over a base cell when a cylindrical algebraic decomposition is lifted by one dimension.

This file develops the stack geometry for arbitrary functions, independently of the polynomials whose roots they will be. Sector j is defined as the set of points lying above exactly the first j sections. When the functions are ordered pointwise this is the region between section j - 1 and section j, and the sections and sectors partition the cylinder. For continuous, strictly ordered functions on a connected base, each sector carries a continuous section, so every part projects onto the whole base, and every section and sector of a real stack is connected. Finally TauCeti.cylinder places the cylinder over a subset S of the coordinate space inside the coordinate space of one more dimension, with the distinguished coordinate first; it is a topological embedding, so connectedness of stack cells transfers to their ambient images, the cells TauCeti.stackCells of the stack in the ambient space.

Main declarations

• TauCeti.sectionSet, TauCeti.sectorSet: the sections and sectors of a stack.
• TauCeti.mem_sectorSet_iff_of_monotone: for ordered functions, a sector is cut out by the two adjacent sections.
• TauCeti.iUnion_sectionSet_union_iUnion_sectorSet, TauCeti.pairwise_disjoint_sectionSet, TauCeti.pairwise_disjoint_sectorSet, TauCeti.disjoint_sectionSet_sectorSet: the sections and sectors partition the cylinder.
• TauCeti.sectionSet_nonempty, TauCeti.sectorSet_nonempty: over a nonempty base, every section and every sector of a strictly ordered stack is nonempty.
• TauCeti.sectorSet_castSucc_succ_eq_image, TauCeti.sectorSet_zero_eq_image, TauCeti.sectorSet_last_eq_image: a bounded sector is the image of X × (0, 1), and the lowest and highest sectors are the images of X × (-∞, 0) and X × (0, ∞), under explicit maps that are continuous whenever the functions of the stack are, for a topological ring α (continuous addition suffices for the two unbounded sectors).
• TauCeti.exists_continuous_forall_mem_sectorSet: every sector of a continuous strictly ordered stack contains the graph of a continuous function.
• TauCeti.isConnected_sectionSet, TauCeti.isConnected_sectorSet: over a connected base, the sections and sectors of a continuous strictly ordered real stack are connected.
• TauCeti.cylinder, TauCeti.isEmbedding_cylinder: the ambient cylinder embedding.
• TauCeti.stackCells: the ambient sections and sectors of a stack over a subset of α ^ n.
• TauCeti.image_cylinder_sectionSet_comp, TauCeti.image_cylinder_sectorSet_comp, TauCeti.stackCells_comp: ambient stack cells pull back along arbitrary base maps.
• TauCeti.stackCells_inclusion: restricting a stack to a subset of its base cuts each ambient cell down to the part lying over that subset.
• TauCeti.sUnion_stackCells, TauCeti.pairwiseDisjoint_stackCells, TauCeti.isConnected_of_mem_stackCells: the ambient cells of a stack partition the cylinder over its base, and over a connected base they are connected.
• TauCeti.ordConnected_setOf_cons_mem_of_mem_stackCells: every ambient cell meets each line parallel to the distinguished axis in an order-connected set.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Section 5.1.

Sections and sectors

def TauCeti.sectionSet {X : Type u_1} {α : Type u_3} {k : ℕ} (θ : Fin k → X → α) (i : Fin k) : Set (X × α)

The i-th section of the stack defined by θ: the graph Function.graph (θ i) of θ i in the cylinder X × α.

@[simp]

theorem TauCeti.mem_sectionSet {X : Type u_1} {α : Type u_3} {k : ℕ} {θ : Fin k → X → α} {i : Fin k} {z : X × α} : z ∈ sectionSet θ i ↔ θ i z.1 = z.2

theorem TauCeti.sectionSet_eq_range {X : Type u_1} {α : Type u_3} {k : ℕ} (θ : Fin k → X → α) (i : Fin k) : sectionSet θ i = Set.range fun (x : X) => (x, θ i x)

A section is the range of the graph map of its function.

theorem TauCeti.sectionSet_comp {X : Type u_1} {Y : Type u_2} {α : Type u_3} {k : ℕ} (θ : Fin k → X → α) (f : Y → X) (i : Fin k) : sectionSet (fun (i : Fin k) => θ i ∘ f) i = Prod.map f id ⁻¹' sectionSet θ i

Sections pull back along a change of base.

@[simp]

theorem TauCeti.fst_image_sectionSet {X : Type u_1} {α : Type u_3} {k : ℕ} (θ : Fin k → X → α) (i : Fin k) : Prod.fst '' sectionSet θ i = Set.univ

Each section lies over the whole base.

@[simp]

theorem TauCeti.sectionSet_nonempty {X : Type u_1} {α : Type u_3} {k : ℕ} [Nonempty X] (θ : Fin k → X → α) (i : Fin k) : (sectionSet θ i).Nonempty

Over a nonempty base, every section is nonempty.

theorem TauCeti.pairwise_disjoint_sectionSet {X : Type u_1} {α : Type u_3} {k : ℕ} {θ : Fin k → X → α} (hθ : ∀ (x : X), Function.Injective fun (i : Fin k) => θ i x) : Pairwise (Function.onFun Disjoint (sectionSet θ))

Distinct sections of a stack whose functions are pointwise injective in the index are disjoint.

def TauCeti.sectorSet {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] (θ : Fin k → X → α) (j : Fin (k + 1)) : Set (X × α)

The j-th sector of the stack defined by θ, for j ≤ k: the points of X × α lying strictly above the first j sections and strictly below the others. When there are no sections the only sector is the whole cylinder.

@[simp]

theorem TauCeti.mem_sectorSet {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] {θ : Fin k → X → α} {j : Fin (k + 1)} {z : X × α} : z ∈ sectorSet θ j ↔ (∀ (i : Fin k), i.castSucc < j → θ i z.1 < z.2) ∧ ∀ (i : Fin k), j ≤ i.castSucc → z.2 < θ i z.1

@[simp]

theorem TauCeti.sectorSet_fin_zero {X : Type u_1} {α : Type u_3} [LinearOrder α] (θ : Fin 0 → X → α) (j : Fin 1) : sectorSet θ j = Set.univ

A stack with no sections has the whole cylinder as its unique sector.

theorem TauCeti.sectorSet_comp {X : Type u_1} {Y : Type u_2} {α : Type u_3} {k : ℕ} [LinearOrder α] (θ : Fin k → X → α) (f : Y → X) (j : Fin (k + 1)) : sectorSet (fun (i : Fin k) => θ i ∘ f) j = Prod.map f id ⁻¹' sectorSet θ j

Sectors pull back along a change of base.

theorem TauCeti.ordConnected_preimage_mk_sectorSet {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] (θ : Fin k → X → α) (j : Fin (k + 1)) (x : X) : (Prod.mk x ⁻¹' sectorSet θ j).OrdConnected

Each fibre of a sector is order-connected: it is an open interval of α, possibly unbounded.

theorem TauCeti.mem_sectorSet_iff_of_monotone {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] {θ : Fin k → X → α} (hθ : ∀ (x : X), Monotone fun (i : Fin k) => θ i x) {j : Fin (k + 1)} {z : X × α} : z ∈ sectorSet θ j ↔ (∀ (i : Fin k), i.succ = j → θ i z.1 < z.2) ∧ ∀ (i : Fin k), i.castSucc = j → z.2 < θ i z.1

For pointwise monotone θ, a point lies in sector j exactly when it is above section j - 1 (if 0 < j) and below section j (if j < k).

theorem TauCeti.sectorSet_zero {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] {θ : Fin (k + 1) → X → α} (hθ : ∀ (x : X), Monotone fun (i : Fin (k + 1)) => θ i x) : sectorSet θ 0 = {z : X × α | z.2 < θ 0 z.1}

For pointwise monotone θ, the lowest sector lies below the lowest section.

theorem TauCeti.sectorSet_last {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] {θ : Fin (k + 1) → X → α} (hθ : ∀ (x : X), Monotone fun (i : Fin (k + 1)) => θ i x) : sectorSet θ (Fin.last (k + 1)) = {z : X × α | θ (Fin.last k) z.1 < z.2}

For pointwise monotone θ, the highest sector lies above the highest section.

theorem TauCeti.sectorSet_castSucc_succ {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] {θ : Fin (k + 1) → X → α} (hθ : ∀ (x : X), Monotone fun (i : Fin (k + 1)) => θ i x) (i : Fin k) : sectorSet θ i.castSucc.succ = {z : X × α | θ i.castSucc z.1 < z.2 ∧ z.2 < θ i.succ z.1}

For pointwise monotone θ, a bounded sector lies between two consecutive sections.

theorem TauCeti.pairwise_disjoint_sectorSet {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] (θ : Fin k → X → α) : Pairwise (Function.onFun Disjoint (sectorSet θ))

Distinct sectors of a stack are disjoint.

theorem TauCeti.disjoint_sectionSet_sectorSet {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] (θ : Fin k → X → α) (i : Fin k) (j : Fin (k + 1)) : Disjoint (sectionSet θ i) (sectorSet θ j)

A section and a sector of a stack are disjoint.

theorem TauCeti.iUnion_sectionSet_union_iUnion_sectorSet {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] {θ : Fin k → X → α} (hθ : ∀ (x : X), Monotone fun (i : Fin k) => θ i x) : (⋃ (i : Fin k), sectionSet θ i) ∪ ⋃ (j : Fin (k + 1)), sectorSet θ j = Set.univ

For pointwise monotone θ, the sections and sectors cover the cylinder.

theorem TauCeti.fst_image_sectorSet {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] {θ : Fin k → X → α} [Nonempty α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] (hθ : ∀ (x : X), StrictMono fun (i : Fin k) => θ i x) (j : Fin (k + 1)) : Prod.fst '' sectorSet θ j = Set.univ

For pointwise strictly monotone θ with values in a densely ordered type without endpoints, each sector lies over the whole base.

theorem TauCeti.sectorSet_nonempty {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] {θ : Fin k → X → α} [Nonempty X] [Nonempty α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] (hθ : ∀ (x : X), StrictMono fun (i : Fin k) => θ i x) (j : Fin (k + 1)) : (sectorSet θ j).Nonempty

Over a nonempty base, every sector of a pointwise strictly monotone stack with values in a densely ordered type without endpoints is nonempty.

Parametrizations of the sectors

theorem TauCeti.sectorSet_castSucc_succ_eq_image {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] [Field α] [IsStrictOrderedRing α] {θ : Fin (k + 1) → X → α} (hθ : ∀ (x : X), StrictMono fun (i : Fin (k + 1)) => θ i x) (i : Fin k) : sectorSet θ i.castSucc.succ = (fun (z : X × α) => (z.1, (AffineMap.lineMap (θ i.castSucc z.1) (θ i.succ z.1)) z.2)) '' Set.univ ×ˢ Set.Ioo 0 1

For pointwise strictly monotone θ with values in an ordered field, the bounded sector between sections i and i + 1 is the image of X × (0, 1) under the map sending (x, s) to the point AffineMap.lineMap (θ i x) (θ (i + 1) x) s of the fibre over x. When α is a topological ring, Continuous.lineMap shows that this map is continuous whenever the functions of the stack are.

theorem TauCeti.sectorSet_zero_eq_image {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] [AddCommGroup α] [IsOrderedAddMonoid α] {θ : Fin (k + 1) → X → α} (hθ : ∀ (x : X), Monotone fun (i : Fin (k + 1)) => θ i x) : sectorSet θ 0 = (fun (z : X × α) => (z.1, θ 0 z.1 + z.2)) '' Set.univ ×ˢ Set.Iio 0

For pointwise monotone θ with values in an ordered additive group, the lowest sector is the image of X × (-∞, 0) under the map translating the height s by θ 0 x. When addition on α is continuous, this map is continuous whenever θ 0 is.

theorem TauCeti.sectorSet_last_eq_image {X : Type u_1} {α : Type u_3} {k : ℕ} [LinearOrder α] [AddCommGroup α] [IsOrderedAddMonoid α] {θ : Fin (k + 1) → X → α} (hθ : ∀ (x : X), Monotone fun (i : Fin (k + 1)) => θ i x) : sectorSet θ (Fin.last (k + 1)) = (fun (z : X × α) => (z.1, θ (Fin.last k) z.1 + z.2)) '' Set.univ ×ˢ Set.Ioi 0

For pointwise monotone θ with values in an ordered additive group, the highest sector is the image of X × (0, ∞) under the map translating the height s by θ k x. When addition on α is continuous, this map is continuous whenever θ k is.

theorem TauCeti.isOpen_sectorSet {X : Type u_1} {α : Type u_3} {k : ℕ} [TopologicalSpace X] {θ : Fin k → X → α} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (hc : ∀ (i : Fin k), Continuous (θ i)) (j : Fin (k + 1)) : IsOpen (sectorSet θ j)

A sector bounded by finitely many continuous functions is open in the cylinder. The functions need not be ordered.

theorem TauCeti.isClosed_sectionSet {X : Type u_1} {α : Type u_3} {k : ℕ} [TopologicalSpace X] {θ : Fin k → X → α} [TopologicalSpace α] [T2Space α] {i : Fin k} (hθ : Continuous (θ i)) : IsClosed (sectionSet θ i)

The section of a continuous function is closed in the cylinder.

theorem TauCeti.isPreconnected_sectionSet {X : Type u_1} {α : Type u_3} {k : ℕ} [TopologicalSpace X] {θ : Fin k → X → α} [TopologicalSpace α] [PreconnectedSpace X] {i : Fin k} (hθ : Continuous (θ i)) : IsPreconnected (sectionSet θ i)

Over a preconnected base, the section of a continuous function is preconnected.

theorem TauCeti.isConnected_sectionSet {X : Type u_1} {α : Type u_3} {k : ℕ} [TopologicalSpace X] {θ : Fin k → X → α} [TopologicalSpace α] [ConnectedSpace X] {i : Fin k} (hθ : Continuous (θ i)) : IsConnected (sectionSet θ i)

Over a connected base, the section of a continuous function is connected.

theorem TauCeti.exists_continuous_forall_mem_sectorSet {X : Type u_1} {α : Type u_3} {k : ℕ} [TopologicalSpace X] {θ : Fin k → X → α} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [TopologicalSpace α] [IsSemitopologicalRing α] (hc : ∀ (i : Fin k), Continuous (θ i)) (hθ : ∀ (x : X), StrictMono fun (i : Fin k) => θ i x) (j : Fin (k + 1)) : ∃ (σ : X → α), Continuous σ ∧ ∀ (x : X), (x, σ x) ∈ sectorSet θ j

Every sector of a stack of continuous, pointwise strictly ordered functions with values in an ordered semitopological field contains the graph of a continuous function.

theorem TauCeti.isPreconnected_sectorSet {X : Type u_1} {k : ℕ} [TopologicalSpace X] {θ : Fin k → X → ℝ} [PreconnectedSpace X] (hc : ∀ (i : Fin k), Continuous (θ i)) (hθ : ∀ (x : X), StrictMono fun (i : Fin k) => θ i x) (j : Fin (k + 1)) : IsPreconnected (sectorSet θ j)

Over a preconnected base, each sector of a stack of continuous, pointwise strictly ordered real functions is preconnected.

theorem TauCeti.isConnected_sectorSet {X : Type u_1} {k : ℕ} [TopologicalSpace X] {θ : Fin k → X → ℝ} [ConnectedSpace X] (hc : ∀ (i : Fin k), Continuous (θ i)) (hθ : ∀ (x : X), StrictMono fun (i : Fin k) => θ i x) (j : Fin (k + 1)) : IsConnected (sectorSet θ j)

Over a connected base, each sector of a stack of continuous, pointwise strictly ordered real functions is connected.

The ambient cylinder

def TauCeti.cylinder {α : Type u_3} {n : ℕ} (S : Set (Fin n → α)) (z : ↑S × α) : Fin (n + 1) → α

The cylinder S × α over a set S of points of α ^ n, placed in α ^ (n + 1) with the distinguished coordinate first.

theorem TauCeti.cylinder_def {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} (z : ↑S × α) : cylinder S z = Fin.cons z.2 ↑z.1

@[simp]

theorem TauCeti.cylinder_apply_zero {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} (z : ↑S × α) : cylinder S z 0 = z.2

@[simp]

theorem TauCeti.cylinder_apply_succ {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} (z : ↑S × α) (i : Fin n) : cylinder S z i.succ = ↑z.1 i

@[simp]

theorem TauCeti.tail_cylinder {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} (z : ↑S × α) : Fin.tail (cylinder S z) = ↑z.1

theorem TauCeti.cylinder_injective {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} : Function.Injective (cylinder S)

Distinct points of the cylinder over S have distinct ambient images.

theorem TauCeti.mem_image_cylinder {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} {A : Set (↑S × α)} {y : Fin (n + 1) → α} : y ∈ cylinder S '' A ↔ ∃ (h : Fin.tail y ∈ S), (⟨Fin.tail y, h⟩, y 0) ∈ A

A point lies in the image of a subset A of the cylinder over S exactly when its last n coordinates lie in S and, together with its distinguished coordinate, give a point of A.

theorem TauCeti.image_tail_image_cylinder {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} (A : Set (↑S × α)) : Fin.tail '' cylinder S '' A = Subtype.val '' Prod.fst '' A

Forgetting the distinguished coordinate of the image of a subset A of the cylinder over S gives the projection of A to S, as a subset of α ^ n.

theorem TauCeti.range_cylinder {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} : Set.range (cylinder S) = {y : Fin (n + 1) → α | Fin.tail y ∈ S}

The cylinder over S fills exactly the points whose last n coordinates lie in S.

theorem TauCeti.continuous_cylinder {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} [TopologicalSpace α] : Continuous (cylinder S)

The cylinder map is continuous.

theorem TauCeti.isEmbedding_cylinder {α : Type u_3} {n : ℕ} {S : Set (Fin n → α)} [TopologicalSpace α] : Topology.IsEmbedding (cylinder S)

The cylinder over S is a topological embedding into α ^ (n + 1).

theorem TauCeti.isOpenEmbedding_tail_image_cylinder_sectionSet {α : Type u_3} {k n : ℕ} {S : Set (Fin n → α)} [TopologicalSpace α] {θ : Fin k → ↑S → α} (i : Fin k) (hc : Continuous (θ i)) : Topology.IsOpenEmbedding fun (y : ↑(cylinder S '' sectionSet θ i)) => ⟨Fin.tail ↑y, ⋯⟩

Forgetting the height identifies an ambient continuous section with its base by an open embedding.

theorem TauCeti.isOpenEmbedding_cons_image_cylinder_sectorSet {k n : ℕ} {S : Set (Fin n → ℝ)} {d : ℕ} {θ : Fin k → ↑S → ℝ} {f : ↑S → Fin d → ℝ} (hf : Topology.IsOpenEmbedding f) (hc : ∀ (i : Fin k), Continuous (θ i)) (j : Fin (k + 1)) : Topology.IsOpenEmbedding fun (y : ↑(cylinder S '' sectorSet θ j)) => Fin.cons (↑y 0) (f ⟨Fin.tail ↑y, ⋯⟩)

An open embedding of the base extends over an ambient sector, retaining the height as the first coordinate.

Stacks in the ambient space

def TauCeti.stackCells {α : Type u_3} {k n : ℕ} [LinearOrder α] (C : Set (Fin n → α)) (θ : Fin k → ↑C → α) : Set (Set (Fin (n + 1) → α))

The cells of the stack over C ⊆ α ^ n defined by θ, as subsets of α ^ (n + 1): the images under TauCeti.cylinder of its k sections and its k + 1 sectors.

@[simp]

theorem TauCeti.mem_stackCells {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {θ : Fin k → ↑C → α} {E : Set (Fin (n + 1) → α)} : E ∈ stackCells C θ ↔ (∃ (i : Fin k), cylinder C '' sectionSet θ i = E) ∨ ∃ (j : Fin (k + 1)), cylinder C '' sectorSet θ j = E

theorem TauCeti.image_cylinder_sectionSet_mem_stackCells {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {θ : Fin k → ↑C → α} (i : Fin k) : cylinder C '' sectionSet θ i ∈ stackCells C θ

theorem TauCeti.image_cylinder_sectorSet_mem_stackCells {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {θ : Fin k → ↑C → α} (j : Fin (k + 1)) : cylinder C '' sectorSet θ j ∈ stackCells C θ

theorem TauCeti.finite_stackCells {α : Type u_3} {k n : ℕ} [LinearOrder α] (C : Set (Fin n → α)) (θ : Fin k → ↑C → α) : (stackCells C θ).Finite

A stack has finitely many cells.

theorem TauCeti.image_cylinder_sectionSet_comp {α : Type u_3} {k n : ℕ} {C : Set (Fin n → α)} {m : ℕ} (θ : Fin k → ↑C → α) (f : (Fin m → α) → Fin n → α) (i : Fin k) : cylinder (f ⁻¹' C) '' sectionSet (fun (i : Fin k) (x : ↑(f ⁻¹' C)) => θ i ⟨f ↑x, ⋯⟩) i = (fun (y : Fin (m + 1) → α) => Fin.cons (y 0) (f (Fin.tail y))) ⁻¹' cylinder C '' sectionSet θ i

Pullback of an ambient section along a base map. The height coordinate is unchanged.

theorem TauCeti.image_cylinder_sectorSet_comp {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {m : ℕ} (θ : Fin k → ↑C → α) (f : (Fin m → α) → Fin n → α) (j : Fin (k + 1)) : cylinder (f ⁻¹' C) '' sectorSet (fun (i : Fin k) (x : ↑(f ⁻¹' C)) => θ i ⟨f ↑x, ⋯⟩) j = (fun (y : Fin (m + 1) → α) => Fin.cons (y 0) (f (Fin.tail y))) ⁻¹' cylinder C '' sectorSet θ j

Pullback of an ambient sector along a base map, including either unbounded sector.

theorem TauCeti.stackCells_comp {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {m : ℕ} (θ : Fin k → ↑C → α) (f : (Fin m → α) → Fin n → α) : (stackCells (f ⁻¹' C) fun (i : Fin k) (x : ↑(f ⁻¹' C)) => θ i ⟨f ↑x, ⋯⟩) = (fun (E : Set (Fin (n + 1) → α)) => (fun (y : Fin (m + 1) → α) => Fin.cons (y 0) (f (Fin.tail y))) ⁻¹' E) '' stackCells C θ

The cells of a pulled-back stack are precisely the inverse images of the original cells. This holds even when the base map is not injective or surjective.

theorem TauCeti.image_cylinder_preimage_inclusion {α : Type u_3} {n : ℕ} {C D : Set (Fin n → α)} (h : D ⊆ C) (A : Set (↑C × α)) : cylinder D '' Prod.map (Set.inclusion h) id ⁻¹' A = cylinder C '' A ∩ Fin.tail ⁻¹' D

Restricting the base of the cylinder from C to a subset D cuts the image of a subset of the cylinder over C down to the points lying over D.

theorem TauCeti.image_cylinder_sectionSet_inclusion {α : Type u_3} {k n : ℕ} {C D : Set (Fin n → α)} (h : D ⊆ C) (θ : Fin k → ↑C → α) (i : Fin k) : cylinder D '' sectionSet (fun (i : Fin k) => θ i ∘ Set.inclusion h) i = cylinder C '' sectionSet θ i ∩ Fin.tail ⁻¹' D

A section of a stack restricted to a smaller base D is the part of the original section lying over D.

theorem TauCeti.image_cylinder_sectorSet_inclusion {α : Type u_3} {k n : ℕ} [LinearOrder α] {C D : Set (Fin n → α)} (h : D ⊆ C) (θ : Fin k → ↑C → α) (j : Fin (k + 1)) : cylinder D '' sectorSet (fun (i : Fin k) => θ i ∘ Set.inclusion h) j = cylinder C '' sectorSet θ j ∩ Fin.tail ⁻¹' D

A sector of a stack restricted to a smaller base D is the part of the original sector lying over D, including either unbounded sector.

theorem TauCeti.stackCells_inclusion {α : Type u_3} {k n : ℕ} [LinearOrder α] {C D : Set (Fin n → α)} (h : D ⊆ C) (θ : Fin k → ↑C → α) : (stackCells D fun (i : Fin k) => θ i ∘ Set.inclusion h) = (fun (x : Set (Fin (n + 1) → α)) => x ∩ Fin.tail ⁻¹' D) '' stackCells C θ

The cells of a stack restricted to a smaller base D are the parts of the original cells lying over D.

theorem TauCeti.image_tail_of_mem_stackCells {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {θ : Fin k → ↑C → α} [Nonempty α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] (hθ : ∀ (x : ↑C), StrictMono fun (i : Fin k) => θ i x) {E : Set (Fin (n + 1) → α)} (hE : E ∈ stackCells C θ) : Fin.tail '' E = C

For pointwise strictly monotone θ with values in a densely ordered type without endpoints, every cell of the stack over C lies over the whole of C.

theorem TauCeti.image_image_tail_iUnion_stackCells {α : Type u_3} {n : ℕ} [LinearOrder α] [Nonempty α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {𝒟 : Set (Set (Fin n → α))} {k : Set (Fin n → α) → ℕ} {θ : (C : Set (Fin n → α)) → Fin (k C) → ↑C → α} (hθ : ∀ C ∈ 𝒟, ∀ (x : ↑C), StrictMono fun (i : Fin (k C)) => θ C i x) : Set.image Fin.tail '' ⋃ C ∈ 𝒟, stackCells C (θ C) = 𝒟

If over each set in 𝒟 a pointwise strictly ordered stack is chosen, with values in a densely ordered type without endpoints, then the projections of all the cells of these stacks are exactly the sets in 𝒟.

theorem TauCeti.sUnion_stackCells {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {θ : Fin k → ↑C → α} (hθ : ∀ (x : ↑C), Monotone fun (i : Fin k) => θ i x) : ⋃₀ stackCells C θ = Fin.tail ⁻¹' C

For pointwise monotone θ, the cells of the stack over C cover the cylinder over C.

theorem TauCeti.pairwiseDisjoint_stackCells {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {θ : Fin k → ↑C → α} (hθ : ∀ (x : ↑C), Function.Injective fun (i : Fin k) => θ i x) : (stackCells C θ).PairwiseDisjoint id

For pointwise injective θ, distinct cells of the stack over C are disjoint.

theorem TauCeti.ordConnected_setOf_cons_mem_of_mem_stackCells {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {θ : Fin k → ↑C → α} {E : Set (Fin (n + 1) → α)} (hE : E ∈ stackCells C θ) (x : Fin n → α) : {t : α | Fin.cons t x ∈ E}.OrdConnected

Every cell of a stack meets each line parallel to the distinguished axis in an order-connected set: a point or nothing for a section, an open interval for a sector.

theorem TauCeti.image_cylinder_preimage_eq {α : Type u_3} {n : ℕ} {C : Set (Fin n → α)} {E : Set (Fin (n + 1) → α)} (hEC : Fin.tail '' E ⊆ C) : cylinder C '' cylinder C ⁻¹' E = E

A set whose projection lies in the base C is recovered from its preimage under the cylinder over C.

theorem TauCeti.eq_stackCells_of_image_cylinder_preimage {α : Type u_3} {k n : ℕ} [LinearOrder α] {C : Set (Fin n → α)} {θ : Fin k → ↑C → α} {𝒞 : Set (Set (Fin (n + 1) → α))} (hθ𝒜 : (fun (x : Set (Fin (n + 1) → α)) => cylinder C ⁻¹' x) '' {E : Set (Fin (n + 1) → α) | E ∈ 𝒞 ∧ Fin.tail '' E = C} = Set.range (sectionSet θ) ∪ Set.range (sectorSet θ)) : {E : Set (Fin (n + 1) → α) | E ∈ 𝒞 ∧ Fin.tail '' E = C} = stackCells C θ

If the preimages under the cylinder over C of the cells of 𝒞 lying over C are exactly the section and sector sets of a stack θ, then these cells are the cells of the stack.

theorem TauCeti.isConnected_of_mem_stackCells {k n : ℕ} {C : Set (Fin n → ℝ)} {θ : Fin k → ↑C → ℝ} (hC : IsConnected C) (hc : ∀ (i : Fin k), Continuous (θ i)) (hθ : ∀ (x : ↑C), StrictMono fun (i : Fin k) => θ i x) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ stackCells C θ) : IsConnected E

For continuous, pointwise strictly monotone real θ over a connected base, every cell of the stack is connected.