Profinite.isIso_of_bijective
theorem Profinite.isIso_of_bijective :
∀ {X Y : Profinite} (f : X ⟶ Y), Function.Bijective ⇑f → CategoryTheory.IsIso f
This theorem states that for any two profinite spaces, `X` and `Y`, a continuous function `f` mapping `X` to `Y` that is also bijective (both injective and surjective) will induce an isomorphism. In other words, a one-to-one and onto mapping between profinite spaces preserves the topology, thereby forming an isomorphism. Thus, the structure of the spaces remains invariant under such a transformation.
More concisely: If two profinite spaces `X` and `Y` are mapped by a continuous, bijective function `f : X → Y`, then `f` induces an isomorphism between them.
|
Profinite.epi_iff_surjective
theorem Profinite.epi_iff_surjective : ∀ {X Y : Profinite} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective ⇑f
This theorem states that for any two Profinite objects `X` and `Y` and a morphism `f` from `X` to `Y`, the morphism `f` is an epimorphism if and only if the function corresponding to `f` is surjective. Here, an epimorphism is a map in category theory that is right-cancellable, and a function is said to be surjective (or onto) if for every element in the codomain, there exists an element in the domain such that applying the function to this element gives the element in the codomain.
More concisely: A profinite morphism between profinite objects is an epimorphism if and only if the corresponding function is surjective.
|
Profinite.isClosedMap
theorem Profinite.isClosedMap : ∀ {X Y : Profinite} (f : X ⟶ Y), IsClosedMap ⇑f
The theorem `Profinite.isClosedMap` states that any morphism, denoted `f`, between two profinite spaces `X` and `Y`, is a closed map. In other words, for any given closed set `U` in `X`, the image of `U` under the morphism `f` is also a closed set in `Y`. This property holds for all morphisms in profinite spaces.
More concisely: The morphism between profinite spaces is a closed map. That is, the image of any closed set under a profinite space morphism is a closed set.
|
Profinite.isTotallyDisconnected
theorem Profinite.isTotallyDisconnected : ∀ (self : Profinite), TotallyDisconnectedSpace ↑self.toCompHaus.toTop := by
sorry
This theorem asserts that every profinite space is totally disconnected. In mathematical terms, for any given profinite space, it can always be interpreted as a totally disconnected topological space. In other words, there are no connected subspaces in a profinite space other than the trivial ones (the empty set and sets containing only a single point).
More concisely: Every profinite space is a totally disconnected topological space.
|