Version 1 source-bound exposition export. Original text SHA-256: 595afd17530ced6ecac85a269dea91694ea5ca0d00d7ce090c2f9de56737e9c6. Link targets are adapted for this edition; the registered Card identity is unchanged. # Continuous finite conjugation relative to a class of source spaces ## Statement This property requires a conjugate $fgf^{-1}$ and its inverse to be fully continuous whenever $f$ and $g$ 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 $h:(X,c)\to(Y,d)$ is fully continuous when $$ h(c(E))\subseteq d(h(E))\qquad(E\subseteq X). \tag{1} $$ Finite continuity requires (1) only for finite $E$. 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 $(X,c)$ be a closure space, and let $D$ be a class of source closure spaces in a fixed universe. For an eligible source $L$ and $t\in L$, let $M=\operatorname{Comp}_L(t)$, 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 $\operatorname{FC}_D(X,c)$ 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 $E\subseteq X$ 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](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/FiniteHomeomorph.lean.html?from=44&start=46&end=50#L46) uses the same outer maps $f$ and $f^{-1}$ in the inverse, not independently chosen maps. The hypotheses in (2) impose full continuity on $f$ and $g$ only. They do not impose full continuity on $f^{-1}$ or $g^{-1}$. Both full-continuity conclusions in (3) are required by the definition. ## Assumptions To form this property one supplies the target closure operator $c$ and the eligible class $D$. In each test, $L$ is any member of $D$, $t$ is any point, and $f,g$ 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 $j:M\hookrightarrow L$ 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 $M$ is not equipped with an independently chosen topology. ## Conclusion The property $\operatorname{FC}_D(X,c)$ 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](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/FiniteConjugation.lean.html?from=44&start=54&end=67#L54) uses exactly $fgf^{-1}$ and its displayed inverse. ## Main citations [Full versus finite continuity](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/Maps.lean.html?from=44&start=29&end=34&ranges=29-34#L29) supplies (1). [The finite conjugate and its inverse](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/FiniteHomeomorph.lean.html?from=44&start=46&end=50#L46) supplies the two maps in (2). [The whole defining right-hand side](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/FiniteConjugation.lean.html?from=44&start=41&end=50#L41) is at lines 41–50; [packaging that same conjugate](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/FiniteConjugation.lean.html?from=44&start=54&end=91&ranges=54-91#L54) is separately at lines 54–91. [Subspace closure](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/Induced.lean.html?from=44&start=97&end=107#L97) gives (4), and [the separate $C^*$-realizability predicate](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/CStarRealization.lean.html#L41) 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. ```lean 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 ``` | In the source | Mathematical meaning | |---|---| | [Target closure and source class](https://exactmathematics.org/mathlibannex/cards/6d987a777ad628da9151adcdfdef5693d121c754b214a7268d4bbb30b2b9677c/versions/gss-r1-0f27ae46ebd2ea45/index.html#card-44--source-row-0)
`def HasContinuousFiniteConjugation (c : ClosureSpace α) (D : ClosureCat.{s} → Prop) : Prop :=` | The input `c` is the closure on $X$ (the source calls its underlying type `α`). The other input specifies the class $D$ of source closure spaces. This defines the condition $\operatorname{FC}_D(X,c)$; it does not assert that the condition holds. | | [All source spaces and all components](https://exactmathematics.org/mathlibannex/cards/6d987a777ad628da9151adcdfdef5693d121c754b214a7268d4bbb30b2b9677c/versions/gss-r1-0f27ae46ebd2ea45/index.html#card-44--source-row-1)
` ∀ (L : ClosureCat.{s}), D L → ∀ t : L,` | Every closure space $L\in D$ and every point $t\in L$ is tested. The component used below is $M=\operatorname{Comp}_L(t)$ with the closure induced from $L$, as in (4). No particular source space or component is selected. | | [The comparison and its forward continuity](https://exactmathematics.org/mathlibannex/cards/6d987a777ad628da9151adcdfdef5693d121c754b214a7268d4bbb30b2b9677c/versions/gss-r1-0f27ae46ebd2ea45/index.html#card-44--source-row-2)
` ∀ f : FiniteHomeomorph (L.str.subspace (L.str.component t)) c,`
` (L.str.subspace (L.str.component t)).Continuous c f.toEquiv →` | The first map is any finite homeomorphism $f:M\to X$. Both occurrences of `L.str.subspace (L.str.component t)` are the same induced closure $c_M$. Separately, for every $E\subseteq M$, $$f(c_M(E))\subseteq c(f(E)).$$ Thus the assumption is forward full continuity of this same $f$, not of $f^{-1}$. | | [The source automorphism and its forward continuity](https://exactmathematics.org/mathlibannex/cards/6d987a777ad628da9151adcdfdef5693d121c754b214a7268d4bbb30b2b9677c/versions/gss-r1-0f27ae46ebd2ea45/index.html#card-44--source-row-3)
` ∀ 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 →` | The second map is any finite homeomorphism $g:M\to M$ on that same component with that same induced closure. It must additionally satisfy, for every $E\subseteq M$, $$g(c_M(E))\subseteq c_M(g(E)).$$ Full continuity of $g^{-1}$ is not assumed. | | [Continuity of the conjugate](https://exactmathematics.org/mathlibannex/cards/6d987a777ad628da9151adcdfdef5693d121c754b214a7268d4bbb30b2b9677c/versions/gss-r1-0f27ae46ebd2ea45/index.html#card-44--source-row-4)
` c.Continuous c (f.conjugate g).toEquiv ∧` | The equivalence `f.conjugate g` has underlying map $h=f\circ g\circ f^{-1}:X\to X$. The first conjunct requires, for every $E\subseteq X$, $$h(c(E))\subseteq c(h(E)).$$ | | [Continuity of the same conjugate inverse](https://exactmathematics.org/mathlibannex/cards/6d987a777ad628da9151adcdfdef5693d121c754b214a7268d4bbb30b2b9677c/versions/gss-r1-0f27ae46ebd2ea45/index.html#card-44--source-row-5)
` c.Continuous c (f.conjugate g).toEquiv.symm` | `symm` gives the inverse of that same equivalence, namely $h^{-1}=f\circ g^{-1}\circ f^{-1}$. The second conjunct requires, for every $E\subseteq X$, $$h^{-1}(c(E))\subseteq c(h^{-1}(E)).$$ The two conjuncts together are (3). | | [Finite-homeomorphism fields](https://exactmathematics.org/mathlibannex/cards/6d987a777ad628da9151adcdfdef5693d121c754b214a7268d4bbb30b2b9677c/versions/gss-r1-0f27ae46ebd2ea45/index.html#card-44--source-row-6)
`structure FiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where`
` finitelyContinuous_toFun : c.FinitelyContinuous d toFun`
` finitelyContinuous_invFun : d.FinitelyContinuous c invFun` | 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 $f:M\to X$ and $g:M\to M$; their additional full-continuity assumptions are separate. | | [The conjugate and its actual inverse](https://exactmathematics.org/mathlibannex/cards/6d987a777ad628da9151adcdfdef5693d121c754b214a7268d4bbb30b2b9677c/versions/gss-r1-0f27ae46ebd2ea45/index.html#card-44--source-row-7)
`def FiniteHomeomorph.conjugate (f : FiniteHomeomorph c d)`
` (g : FiniteHomeomorph c c) : FiniteHomeomorph d d :=`
` f.symm.trans (g.trans f)` | The conjugate is formed from the same finite homeomorphisms $f$ and $g$. Composition sends $x\in X$ first by $f^{-1}$, then by $g$, then by $f$. Its inverse uses $g^{-1}$ between those same outer maps, as displayed in (2). | The baseline's old range 41–53 and its header-only signature fingerprint are retained as historical records. The new binding fingerprints the full definition 41–50 separately. The retained printed type for this definition is **not** elided; it records the type of the definition, not a replacement for its defining right-hand side. No new parser or census was run. ### Source context (separate exact excerpt) These are independent ambient excerpts. ```lean universe u v w s t ``` ```lean variable {α : Type u} {β : Type v} {γ : Type w} variable {c : ClosureSpace α} {d : ClosureSpace β} {k : ClosureSpace γ} ``` 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.