Stonean.Sigma.openEmbedding_ι
theorem Stonean.Sigma.openEmbedding_ι :
∀ {α : Type} [inst : Finite α] (Z : α → Stonean) (a : α), OpenEmbedding ⇑(CategoryTheory.Limits.Sigma.ι Z a) := by
sorry
This theorem states that for any type `α` that is finite, and any function `Z` from `α` to `Stonean` (a type representing a Stonean space), the inclusion maps into the abstract finite coproduct are open embeddings. More specifically, for any element `a` of `α`, the function represented by `CategoryTheory.Limits.Sigma.ι Z a` is an open embedding. In the language of category theory, an open embedding is a morphism that induces a homeomorphism onto its image and such that the preimage of any open set is open. In this context, it means that the inclusion map (which sends each element of the index set to its corresponding part in the coproduct) is continuous, and its inverse map is also continuous when restricted to the image of the inclusion map.
More concisely: For any finite type `α` and function `Z : α → Stonean`, the inclusion maps `CategoryTheory.Limits.Sigma.ι Z a : {x : Stonean | ∃ i : α, Z i = x} → Stonean` are open embeddings.
|
Stonean.finiteCoproduct.openEmbedding_ι
theorem Stonean.finiteCoproduct.openEmbedding_ι :
∀ {α : Type} [inst : Finite α] (Z : α → Stonean) (a : α), OpenEmbedding ⇑(Stonean.finiteCoproduct.ι Z a)
This theorem states that for any type `α` which is finite and for any function `Z` mapping from `α` to the mathematical structure called Stonean, the corresponding inclusion map into the finite coproduct, denoted by `Stonean.finiteCoproduct.ι Z a`, is an open embedding. This means that not only is the map injective and its image is a topological subspace, but also the map itself preserves the topology in the sense that a set is open in the source space if and only if its image is open in the destination space.
More concisely: Given a finite type `α` and a function `Z : α → Stonean`, the inclusion map `Stonean.finiteCoproduct.ι Z : ⋃i:α. Z i → ⨄i:α. Stonean Z i` is an open embedding.
|