Coordinate zero-pattern strata

For a subset A of an index type, the corresponding zero-pattern stratum consists of families that vanish exactly on A, paired with an unrestricted second component. This file records the product description of these strata, their local closedness when only finitely many coordinates are required to be nonzero, and their closure when zero is not isolated.

Main declarations

• TauCeti.zeroPatternSet: the coordinate stratum with zero set exactly A.
• TauCeti.isLocallyClosed_zeroPatternSet: a zero-pattern stratum with finitely many nonzero coordinates is locally closed.
• TauCeti.closure_zeroPatternSet: its closure allows additional coordinates to vanish.
• TauCeti.zeroPatternSetHomeomorph: its nonzero coordinates give product coordinates.

def TauCeti.zeroPatternSet (α : Type u_1) (β : Type u_2) (K : Type u_3) [Zero K] (A : Set α) : Set ((α → K) × β)

The coordinate stratum attached to a subset A of an index type: precisely those pairs whose first coordinates vanish on A and nowhere else. The second component is unrestricted.

@[simp]

theorem TauCeti.mem_zeroPatternSet {α : Type u_1} {β : Type u_2} {K : Type u_3} [Zero K] {A : Set α} {z : (α → K) × β} : z ∈ zeroPatternSet α β K A ↔ ∀ (a : α), z.1 a = 0 ↔ a ∈ A

A coordinate pair belongs to the stratum attached to A exactly when its first coordinate vanishes precisely on A.

theorem TauCeti.zeroPatternSet_eq_pi_prod {α : Type u_1} {β : Type u_2} {K : Type u_3} [Zero K] (A : Set α) : zeroPatternSet α β K A = (Set.univ.pi fun (a : α) => {z : K | z = 0 ↔ a ∈ A}) ×ˢ Set.univ

The coordinate stratum is a product of single-coordinate conditions with an unrestricted second factor.

noncomputable def TauCeti.zeroPatternSetHomeomorph (α : Type u_1) (β : Type u_2) (K : Type u_3) [Zero K] [TopologicalSpace K] [TopologicalSpace β] (A : Set α) : ↑(zeroPatternSet α β K A) ≃ₜ ({ a : α // a ∉ A } → { z : K // z ≠ 0 }) × β

A zero-pattern stratum is the space of nonzero coordinates outside its zero set, together with its unrestricted second factor. This description retains the subspace topology.

@[simp]

theorem TauCeti.val_zeroPatternSetHomeomorph_fst_apply {α : Type u_1} {β : Type u_2} {K : Type u_3} [Zero K] [TopologicalSpace K] [TopologicalSpace β] {A : Set α} (z : ↑(zeroPatternSet α β K A)) (a : { a : α // a ∉ A }) : ↑(((zeroPatternSetHomeomorph α β K A) z).1 a) = (↑z).1 ↑a

The homeomorphism retains each coordinate outside the prescribed zero set.

@[simp]

theorem TauCeti.zeroPatternSetHomeomorph_snd_apply {α : Type u_1} {β : Type u_2} {K : Type u_3} [Zero K] [TopologicalSpace K] [TopologicalSpace β] {A : Set α} (z : ↑(zeroPatternSet α β K A)) : ((zeroPatternSetHomeomorph α β K A) z).2 = (↑z).2

The unrestricted factor is unchanged by the zero-pattern homeomorphism.

@[simp]

theorem TauCeti.zeroPatternSetHomeomorph_symm_fst_apply_of_mem {α : Type u_1} {β : Type u_2} {K : Type u_3} [Zero K] [TopologicalSpace K] [TopologicalSpace β] {A : Set α} (w : ({ a : α // a ∉ A } → { z : K // z ≠ 0 }) × β) {a : α} (ha : a ∈ A) : (↑((zeroPatternSetHomeomorph α β K A).symm w)).1 a = 0

The inverse fills the prescribed zero coordinates with zero.

@[simp]

theorem TauCeti.zeroPatternSetHomeomorph_symm_fst_apply_of_notMem {α : Type u_1} {β : Type u_2} {K : Type u_3} [Zero K] [TopologicalSpace K] [TopologicalSpace β] {A : Set α} (w : ({ a : α // a ∉ A } → { z : K // z ≠ 0 }) × β) {a : α} (ha : a ∉ A) : (↑((zeroPatternSetHomeomorph α β K A).symm w)).1 a = ↑(w.1 ⟨a, ha⟩)

Outside the zero set, the inverse restores the retained coordinate.

@[simp]

theorem TauCeti.zeroPatternSetHomeomorph_symm_snd_apply {α : Type u_1} {β : Type u_2} {K : Type u_3} [Zero K] [TopologicalSpace K] [TopologicalSpace β] {A : Set α} (w : ({ a : α // a ∉ A } → { z : K // z ≠ 0 }) × β) : (↑((zeroPatternSetHomeomorph α β K A).symm w)).2 = w.2

The inverse also leaves the unrestricted factor unchanged.

theorem TauCeti.isLocallyClosed_zeroPatternSet {α : Type u_1} {β : Type u_2} {K : Type u_3} [Zero K] [TopologicalSpace K] [T1Space K] [TopologicalSpace β] {A : Set α} (hA : Aᶜ.Finite) : IsLocallyClosed (zeroPatternSet α β K A)

A coordinate stratum is locally closed when only finitely many first coordinates are required to be nonzero.

theorem TauCeti.closure_zeroPatternSet {α : Type u_1} {β : Type u_2} {K : Type u_3} [Zero K] [TopologicalSpace K] [T1Space K] [(nhdsWithin 0 {0}ᶜ).NeBot] [TopologicalSpace β] (A : Set α) : closure (zeroPatternSet α β K A) = {z : (α → K) × β | ∀ a ∈ A, z.1 a = 0}

The closure of a coordinate stratum permits additional first coordinates to vanish, while retaining the coordinates already forced to be zero.