Continuous finite conjugation relative to a class of source spaces

ClosureSpace.HasContinuousFiniteConjugation

def

Defines when finite conjugation is continuous in both directions.

Statement

This property requires a conjugate and its inverse to be fully continuous whenever and satisfy the finite-continuity and forward full-continuity conditions below. The requirement ranges over every component of every closure space in a specified class.

A closure operator here is extensive, monotone, idempotent, and sends the empty set to the empty set. It need not satisfy the finite-union axiom of topological closure. A map is fully continuous when

h(c(E))\subseteq d(h(E))\qquad(E\subseteq X). \tag{1}

Finite continuity requires (1) only for finite . A finite-homeomorphism is a bijection for which both the map and its inverse are finitely continuous; neither is thereby assumed fully continuous.

Definition

Let be a closure space, and let be a class of source closure spaces in a fixed universe. For an eligible source and , let , equipped with its subspace closure. Components are generated by pairs which are not already closed, together with equality; they are not assumed to be topological connected components or closed subsets.

The property holds when the following universally quantified requirement holds:

\begin{gathered} \text{for every }L\in D,\quad t\in L,\quad M=\operatorname{Comp}_L(t),\\ \text{for every finite-homeomorphism } f:M\longrightarrow X \text{ with }f\text{ fully continuous},\\ \text{for every finite-homeomorphism } g:M\longrightarrow M \text{ with }g\text{ fully continuous},\\[2pt] h=f\circ g\circ f^{-1}\text{ and }h^{-1}=f\circ g^{-1}\circ f^{-1} \text{ are fully continuous on }(X,c). \end{gathered} \tag{2}

Both conclusions are part of the defining conjunction. Explicitly, for every they require

\begin{aligned} h(c(E))&\subseteq c(h(E)),\\ h^{-1}(c(E))&\subseteq c(h^{-1}(E)). \end{aligned} \tag{3}

The finite-conjugation construction uses the same outer maps and in the inverse, not independently chosen maps.

The hypotheses in (2) impose full continuity on and only. They do not impose full continuity on or . Both full-continuity conclusions in (3) are required by the definition.

Assumptions

To form this property one supplies the target closure operator and the eligible class . In each test, is any member of , is any point, and are any finite-homeomorphisms satisfying the two stated forward full-continuity conditions. No eligible source, point, or map is existentially selected by the definition. If there are no qualifying tests, the universal requirement holds vacuously; the definition asserts no realization or existence theorem.

If denotes the inclusion, the source closure used in both map hypotheses is

c_M(E)=j^{-1}\bigl(c_L(j(E))\bigr)\qquad(E\subseteq M). \tag{4}

It is not replaced by a closure generated only by finite sets, and is not equipped with an independently chosen topology.

Conclusion

The property is defined by all of (2), including both lines of (3); it need not hold for every closure space. When it holds, the full conjugation homeomorphism uses exactly and its displayed inverse.

Main citations

Full versus finite continuity supplies (1). The finite conjugate and its inverse supplies the two maps in (2). The whole defining right-hand side is at lines 41–50; packaging that same conjugate is separately at lines 54–91. Subspace closure gives (4), and the separate -realizability predicate specifies the eligible class in the application.

Lean source signature (exact)

For this definition the exact excerpt includes the entire right-hand side. The following declaration is separate.

def HasContinuousFiniteConjugation (c : ClosureSpace α) (D : ClosureCat.{s} → Prop) : Prop :=
  ∀ (L : ClosureCat.{s}), D L → ∀ t : L,
    ∀ f : FiniteHomeomorph (L.str.subspace (L.str.component t)) c,
      (L.str.subspace (L.str.component t)).Continuous c f.toEquiv →
      ∀ g : FiniteHomeomorph (L.str.subspace (L.str.component t))
          (L.str.subspace (L.str.component t)),
        (L.str.subspace (L.str.component t)).Continuous
          (L.str.subspace (L.str.component t)) g.toEquiv →
        c.Continuous c (f.conjugate g).toEquiv ∧
          c.Continuous c (f.conjugate g).toEquiv.symm

Back to the reading-guide item

In the source	Mathematical meaning
Target closure and source class`def HasContinuousFiniteConjugation (c : ClosureSpace α) (D : ClosureCat.{s} → Prop) : Prop :=`Fixed source	The input `c` is the closure on (the source calls its underlying type `α`). The other input specifies the class of source closure spaces. This defines the condition ; it does not assert that the condition holds.
All source spaces and all components`∀ (L : ClosureCat.{s}), D L → ∀ t : L,`Fixed source	Every closure space and every point is tested. The component used below is with the closure induced from , as in (4). No particular source space or component is selected.
The comparison and its forward continuity`∀ f : FiniteHomeomorph (L.str.subspace (L.str.component t)) c, (L.str.subspace (L.str.component t)).Continuous c f.toEquiv →`Fixed source	The first map is any finite homeomorphism . Both occurrences of `L.str.subspace (L.str.component t)` are the same induced closure . Separately, for every , $f(c_M(E))\subseteq c(f(E)).$ Thus the assumption is forward full continuity of this same , not of .
The source automorphism and its forward continuity`∀ g : FiniteHomeomorph (L.str.subspace (L.str.component t)) (L.str.subspace (L.str.component t)), (L.str.subspace (L.str.component t)).Continuous (L.str.subspace (L.str.component t)) g.toEquiv →`Fixed source	The second map is any finite homeomorphism on that same component with that same induced closure. It must additionally satisfy, for every , $g(c_M(E))\subseteq c_M(g(E)).$ Full continuity of is not assumed.
Continuity of the conjugate`c.Continuous c (f.conjugate g).toEquiv ∧`Fixed source	The equivalence `f.conjugate g` has underlying map . The first conjunct requires, for every , $h(c(E))\subseteq c(h(E)).$
Continuity of the same conjugate inverse`c.Continuous c (f.conjugate g).toEquiv.symm`Fixed source	`symm` gives the inverse of that same equivalence, namely . The second conjunct requires, for every , $h^{-1}(c(E))\subseteq c(h^{-1}(E)).$ The two conjuncts together are (3).
Finite-homeomorphism fields`structure FiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where finitelyContinuous_toFun : c.FinitelyContinuous d toFun finitelyContinuous_invFun : d.FinitelyContinuous c invFun`Fixed source	The inherited equivalence supplies a bijection and its inverse. Both fields impose closure continuity only on finite subsets, as defined in the Statement. These fields are used for and ; their additional full-continuity assumptions are separate.
The conjugate and its actual inverse`def FiniteHomeomorph.conjugate (f : FiniteHomeomorph c d) (g : FiniteHomeomorph c c) : FiniteHomeomorph d d := f.symm.trans (g.trans f)`Fixed source	The conjugate is formed from the same finite homeomorphisms and . Composition sends first by , then by , then by . Its inverse uses between those same outer maps, as displayed in (2).

Exact surrounding source context (separate excerpts)

These are independent ambient excerpts.

universe u v w s t

Back to the reading-guide item

variable {α : Type u} {β : Type v} {γ : Type w}
variable {c : ClosureSpace α} {d : ClosureSpace β} {k : ClosureSpace γ}

Back to the reading-guide item

The selected definition uses the carrier α and explicitly supplies its own c, together with source universe s. The surrounding β, γ, d, and k serve later transport declarations and are not additional inputs to this definition. No following declaration's local hypotheses are imported into its scope.

Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·

Technical documentation