ProCGroups.InverseSystems.ProjectionImageSystems
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
def InverseSystem.projectionImageSystem {I : Type u} [Preorder I]
(S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
InverseSystem (I := I) where
X := fun i => S.projection i '' Y
topologicalSpace := fun _ => inferInstance
map := fun {i j} hij x => ⟨S.map hij x.1, by
rcases x.2 with ⟨y, hy, hxy⟩
refine ⟨y, hy, ?_⟩
simpa [← hxy] using (S.projection_compatible y i j hij).symm⟩
continuous_map := fun {i j} hij =>
Continuous.subtype_mk
((S.continuous_map hij).comp continuous_subtype_val) (fun x => by
rcases x.2 with ⟨y, hy, hxy⟩
refine ⟨y, hy, ?_⟩
simpa [Function.comp, ← hxy] using (S.projection_compatible y i j hij).symm)
map_id := fun i => by
funext x
apply Subtype.ext
simp only [map_id_apply, id_eq]
map_comp := fun {i j k} hij hjk => by
funext x
apply Subtype.ext
simp only [Function.comp_apply, S.map_comp_apply hij hjk]The inverse system formed by the projection images of a subset of an inverse limit.
def projectionImageInclusion {I : Type u} [Preorder I]
(S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
(S.projectionImageSystem Y).Morphism S where
map := fun _ => Subtype.val
continuous_map := fun _ => continuous_subtype_val
comm := fun {i j} hij => by
funext x
rflThe canonical morphism from the projection-image system into the ambient inverse system.
def projectionImageSectionMap {I : Type u} [Preorder I]
(S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :
Y → (S.projectionImageSystem Y).X i :=
fun y => ⟨S.projection i y.1, ⟨y.1, y.2, rfl⟩⟩The coordinatewise section map from a subset of an inverse limit to its projection-image system.
theorem continuous_projectionImageSectionMap {I : Type u} [Preorder I]
(S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :
Continuous (projectionImageSectionMap S Y i)The section map from the projection-image inverse limit back to the closed subspace is continuous.
Show proof
by
exact Continuous.subtype_mk ((S.continuous_projection i).comp continuous_subtype_val)
(fun y => ⟨y.1, y.2, rfl⟩)Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem compatible_projectionImageSectionMap {I : Type u} [Preorder I]
(S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
(S.projectionImageSystem Y).CompatibleMaps (projectionImageSectionMap S Y)The projection-image section maps are compatible with the inverse-system transition maps.
Show proof
by
intro i j hij
funext y
apply Subtype.ext
exact S.projection_compatible y.1 i j hijProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem surjective_projectionImageSectionMap {I : Type u} [Preorder I]
(S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :
Function.Surjective (projectionImageSectionMap S Y i)Each coordinate section map onto a projection image is surjective.
Show proof
by
intro x
rcases x.2 with ⟨y, hy, hxy⟩
refine ⟨⟨y, hy⟩, ?_⟩
apply Subtype.ext
simpa using hxyProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□def projectionImageLift {I : Type u} [Preorder I]
(S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
Y → (S.projectionImageSystem Y).inverseLimit :=
(S.projectionImageSystem Y).inverseLimitLift (projectionImageSectionMap S Y)
(compatible_projectionImageSectionMap S Y)The canonical lift from a subset of an inverse limit to the inverse limit of its projection-image system.
theorem continuous_projectionImageLift {I : Type u} [Preorder I]
(S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
Continuous (projectionImageLift S Y)The lift from a closed subspace into the inverse limit of its projection images is continuous.
Show proof
by
exact (S.projectionImageSystem Y).continuous_inverseLimitLift (projectionImageSectionMap S Y)
(continuous_projectionImageSectionMap S Y) (compatible_projectionImageSectionMap S Y)Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem surjective_projectionImageLift {I : Type u} [Preorder I] [Nonempty I]
(S : InverseSystem (I := I)) [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I)) (Y : Set S.inverseLimit) (hY : IsClosed Y) :
Function.Surjective (projectionImageLift S Y)For a closed subset of a compact Hausdorff inverse limit, the canonical projection-image lift is surjective.
Show proof
by
let T := S.projectionImageSystem Y
letI : CompactSpace Y := by
simpa using hY.isClosedEmbedding_subtypeVal.compactSpace
letI : ∀ i, T2Space (T.X i) := fun i => by
change T2Space (S.projection i '' Y)
infer_instance
exact T.surjective_inverseLimitLift (projectionImageSectionMap S Y) (continuous_projectionImageSectionMap S Y)
(compatible_projectionImageSectionMap S Y) (surjective_projectionImageSectionMap S Y) hdirProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem projectionImageLift_comp_subtype {I : Type u} [Preorder I]
(S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
(S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) ∘
projectionImageLift S Y = Subtype.valComposing the projection-image lift with the inclusion morphism recovers the underlying point of the original inverse limit.
Show proof
by
funext y
apply S.ext
intro i
have hpi :
(S.projectionImageSystem Y).projection i (projectionImageLift S Y y) =
projectionImageSectionMap S Y i y := by
simpa [Function.comp, projectionImageLift] using
congrFun
((S.projectionImageSystem Y).projection_comp_inverseLimitLift (projectionImageSectionMap S Y)
(compatible_projectionImageSectionMap S Y) i) y
calc
S.projection i ((S.projectionImageSystem Y).limMap (projectionImageInclusion S Y)
(projectionImageLift S Y y))
= (projectionImageInclusion S Y).map i
((S.projectionImageSystem Y).projection i (projectionImageLift S Y y)) := by
simpa [Function.comp] using
congrFun
((S.projectionImageSystem Y).π_comp_limMap
(Θ := projectionImageInclusion S Y) i) (projectionImageLift S Y y)
_ = ((S.projectionImageSystem Y).projection i (projectionImageLift S Y y)).1 := rfl
_ = (projectionImageSectionMap S Y i y).1 := by rw [hpi]
_ = S.projection i y.1 := rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem InverseSystem.surjective_projectionImageSystem_map
{I : Type u} [Preorder I] (S : InverseSystem (I := I)) (Y : Set S.inverseLimit)
{i j : I} (hij : i ≤ j) :
Function.Surjective ((S.projectionImageSystem Y).map hij)The transition maps in the projection-image system are always surjective.
Show proof
by
intro x
rcases x.2 with ⟨y, hy, hxy⟩
refine ⟨⟨S.projection j y, ⟨y, hy, rfl⟩⟩, ?_⟩
apply Subtype.ext
change S.map hij (S.projection j y) = x.1
rw [S.projection_compatible y i j hij]
exact hxyProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□noncomputable def InverseSystem.homeomorph_projectionImageSystem_of_isClosed
{I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(Y : Set S.inverseLimit) (hY : IsClosed Y) :
Y ≃ₜ (S.projectionImageSystem Y).inverseLimit := by
classical
letI : CompactSpace Y := by
simpa using hY.isClosedEmbedding_subtypeVal.compactSpace
letI : ∀ i, T2Space ((S.projectionImageSystem Y).X i) := fun i => by
change T2Space (S.projection i '' Y)
infer_instance
let e := projectionImageLift S Y
have he_inj : Function.Injective e := by
intro y y' hyy
have hy : y.1 = y'.1 := by
calc
y.1 = (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) (e y) := by
simpa [Function.comp] using (congrFun (projectionImageLift_comp_subtype S Y) y).symm
_ = (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) (e y') := by
rw [hyy]
_ = y'.1 := by
simpa [Function.comp] using congrFun (projectionImageLift_comp_subtype S Y) y'
exact Subtype.ext hy
exact (continuous_projectionImageLift S Y).homeoOfBijectiveCompactToT2
⟨he_inj, surjective_projectionImageLift S hdir Y hY⟩A closed subset of an inverse limit is homeomorphic to the inverse limit of its projection-image system.
theorem range_limMap_projectionImageInclusion_eq
{I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(Y : Set S.inverseLimit) (hY : IsClosed Y) :
Set.range ((S.projectionImageSystem Y).limMap (projectionImageInclusion S Y)) = YThe range of the limit map is exactly the compatible inverse limit of the projection images.
Show proof
by
classical
apply le_antisymm
· rintro x ⟨z, rfl⟩
rcases surjective_projectionImageLift S hdir Y hY z with ⟨y, hy⟩
have hx :
(S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) z = y.1 := by
calc
(S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) z
= (S.projectionImageSystem Y).limMap
(projectionImageInclusion S Y) (projectionImageLift S Y y) := by
rw [hy]
_ = y.1 := by
simpa [Function.comp] using congrFun (projectionImageLift_comp_subtype S Y) y
exact hx ▸ y.2
· intro y hy
refine ⟨projectionImageLift S Y ⟨y, hy⟩, ?_⟩
simpa [Function.comp] using congrFun (projectionImageLift_comp_subtype S Y) ⟨y, hy⟩Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem InverseSystem.mem_isClosed_iff_forall_projection_mem
{I : Type u} [Preorder I] {S : InverseSystem (I := I)} [Nonempty I]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
{Y : Set S.inverseLimit} (hY : IsClosed Y) {x : S.inverseLimit} :
x ∈ Y ↔ ∀ i, S.projection i x ∈ S.projection i '' YMembership in the projected image system can be checked coordinatewise.
Show proof
by
classical
constructor
· intro hx i
exact ⟨x, hx, rfl⟩
· intro hx
let T := S.projectionImageSystem Y
let incl : T.Morphism S := projectionImageInclusion S Y
have hcompat :
T.CompatibleMaps (fun (i : I) (_ : Unit) => (⟨S.projection i x, hx i⟩ : T.X i)) := by
intro i j hij
funext _
apply Subtype.ext
exact S.projection_compatible x i j hij
let z : T.inverseLimit :=
T.inverseLimitLift (fun (i : I) (_ : Unit) => (⟨S.projection i x, hx i⟩ : T.X i)) hcompat ()
have hz : T.limMap incl z = x := by
apply S.ext
intro i
have hpi : T.projection i z = (⟨S.projection i x, hx i⟩ : T.X i) := by
simpa [Function.comp, z] using
congrFun
(T.projection_comp_inverseLimitLift (fun (i : I) (_ : Unit) => (⟨S.projection i x, hx i⟩ : T.X i)) hcompat i) ()
calc
S.projection i (T.limMap incl z) = incl.map i (T.projection i z) := by
simpa [Function.comp] using congrFun (T.π_comp_limMap (Θ := incl) i) z
_ = (T.projection i z).1 := rfl
_ = S.projection i x := by rw [hpi]
have hxrange : x ∈ Set.range (T.limMap incl) := ⟨z, hz⟩
rw [range_limMap_projectionImageInclusion_eq S hdir Y hY] at hxrange
exact hxrangeProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem InverseSystem.exists_homeomorph_closed_subspace_projection_images
{I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(Y : Set S.inverseLimit) (hY : IsClosed Y) :
(∀ i, Nonempty (((S.projectionImageSystem Y).X i) ≃ₜ (S.projection i '' Y))) ∧
Nonempty (Y ≃ₜ (S.projectionImageSystem Y).inverseLimit)A closed subspace of an inverse limit is again an inverse limit of its projection images.
Show proof
by
constructor
· intro i
exact ⟨Homeomorph.refl _⟩
· exact ⟨S.homeomorph_projectionImageSystem_of_isClosed hdir Y hY⟩Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem InverseSystem.projection_image_closure_eq_closure_projection_image
{I : Type u} [Preorder I] (S : InverseSystem (I := I))
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(i : I) (Y : Set S.inverseLimit) :
S.projection i '' closure Y = closure (S.projection i '' Y)The projection of the closure of a subset equals the closure of the projection image.
Show proof
by
let hclosed : IsClosedMap (S.projection i) := (S.continuous_projection i).isClosedMap
simpa using (hclosed.closure_image_eq_of_continuous (S.continuous_projection i) Y).symm
/-
Textual note: the printed PDF on p. 7 states these results without closures on the projection
images. As written, that is false already for a one-point index set. The proof works after
inserting closures on the projection images, equivalently by replacing `Y` with `closure Y`
inside the projection-image system.
-/Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem InverseSystem.exists_homeomorph_closure_projection_images
{I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(Y : Set S.inverseLimit) :
(∀ i, Nonempty (((S.projectionImageSystem (closure Y)).X i) ≃ₜ (S.projection i '' closure Y))) ∧
Nonempty (closure Y ≃ₜ (S.projectionImageSystem (closure Y)).inverseLimit)The closure of a subset of an inverse limit is homeomorphic to the inverse limit of the projection-image system of that closure.
Show proof
by
simpa using S.exists_homeomorph_closed_subspace_projection_images hdir (Y := closure Y)
isClosed_closureProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem InverseSystem.closure_eq_of_projection_images_eq
{I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(Y Y' : Set S.inverseLimit)
(hproj : ∀ i, S.projection i '' closure Y = S.projection i '' closure Y') :
closure Y = closure Y'Closed subsets of the inverse limit are equal when their projection images agree at every stage.
Show proof
by
ext x
constructor
· intro hx
rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure] at hx
rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
intro i
rw [← hproj i]
exact hx i
· intro hx
rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure] at hx
rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
intro i
rw [hproj i]
exact hx iProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem InverseSystem.closure_eq_of_projection_images_eq_of_subsets
{I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(Y Y' : Set S.inverseLimit)
(hproj : ∀ i, S.projection i '' Y = S.projection i '' Y') :
closure Y = closure Y'Equal raw projection images of two subsets force their closures in the inverse limit to be equal.
Show proof
by
apply S.closure_eq_of_projection_images_eq hdir Y Y'
intro i
calc
S.projection i '' closure Y = closure (S.projection i '' Y) := by
exact S.projection_image_closure_eq_closure_projection_image i Y
_ = closure (S.projection i '' Y') := by rw [hproj i]
_ = S.projection i '' closure Y' := by
symm
exact S.projection_image_closure_eq_closure_projection_image i Y'Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□noncomputable def InverseSystem.homeomorph_surjectiveProjectionImageSystem
{I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I)) :
S.inverseLimit ≃ₜ (S.projectionImageSystem (Set.univ : Set S.inverseLimit)).inverseLimit :=
(Homeomorph.Set.univ S.inverseLimit).symm.trans
(S.homeomorph_projectionImageSystem_of_isClosed hdir Set.univ isClosed_univ)Any inverse system of compact Hausdorff spaces admits a surjective projection-image system with the same inverse limit.
theorem InverseSystem.exists_homeomorph_surjectiveProjectionImageSystem
{I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I)) :
(∀ {i j : I} (hij : i ≤ j),
Function.Surjective ((S.projectionImageSystem (Set.univ : Set S.inverseLimit)).map hij)) ∧
Nonempty (S.inverseLimit ≃ₜ
(S.projectionImageSystem (Set.univ : Set S.inverseLimit)).inverseLimit)The projection-image system of the full inverse limit is surjective and has the same inverse limit as the original system.
Show proof
by
constructor
· intro i j hij
exact S.surjective_projectionImageSystem_map (Y := (Set.univ : Set S.inverseLimit)) hij
· exact ⟨S.homeomorph_surjectiveProjectionImageSystem hdir⟩Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□