Module

ProjectionImageSystems.lean

Nyll.ProCGroups.InverseSystems.ProjectionImageSystems

21 declarations indexed from sourceView source ↗

Module documentation

Inverse systems formed from projection images

A subset of an inverse limit determines an inverse system of its stagewise projection images. This module constructs the comparison lift, proves reconstruction for closed subsets of compact Hausdorff systems, and derives closure and equality criteria from stagewise images. It also handles systems whose transition maps are surjective by identifying their projection images.

Imports1

Nyll.ProCGroups.InverseSystems.CofinalityAndDensity

Imported by3

def

projectionImageSystem

L26 ↗

ProCGroups.InverseSystems.InverseSystem.projectionImageSystem

Documentation

The inverse system formed by the projection images of a subset of an inverse limit.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · full declaration

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, ?_⟩
    exact (S.projection_compatible y i j hij).symm.trans (congrArg (S.map hij) hxy)⟩
  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, ?_⟩
        exact (S.projection_compatible y i j hij).symm.trans (congrArg (S.map hij) hxy))
  map_id := fun i => by
    funext x
    apply Subtype.ext
    change S.map (le_rfl : i ≤ i) x.val = x.val
    exact S.map_id_apply i x.val
  map_comp := fun {i j k} hij hjk => by
    funext x
    apply Subtype.ext
    change S.map hij (S.map hjk x.val) = S.map (hij.trans hjk) x.val
    exact S.map_comp_apply hij hjk x.val

def

projectionImageInclusion

L53 ↗

ProCGroups.InverseSystems.projectionImageInclusion

Documentation

The canonical morphism from the projection-image system into the ambient inverse system.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · full declaration

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
    rfl

def

projectionImageSectionMap

L65 ↗

ProCGroups.InverseSystems.projectionImageSectionMap

Documentation

The coordinatewise section map from a subset of an inverse limit to its projection-image system.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

def projectionImageSectionMap {I : Type u} [Preorder I]
    (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :
    Y → (S.projectionImageSystem Y).X i

theorem

continuous_projectionImageSectionMap

L74 ↗

ProCGroups.InverseSystems.continuous_projectionImageSectionMap

Documentation

The section map from the projection-image inverse limit back to the closed subspace is continuous.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

theorem continuous_projectionImageSectionMap {I : Type u} [Preorder I]
    (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :
    Continuous (projectionImageSectionMap S Y i)

theorem

compatible_projectionImageSectionMap

L81 ↗

ProCGroups.InverseSystems.compatible_projectionImageSectionMap

Documentation

The projection-image section maps are compatible with the inverse-system transition maps.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

theorem compatible_projectionImageSectionMap {I : Type u} [Preorder I]
    (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
    (S.projectionImageSystem Y).CompatibleMaps (projectionImageSectionMap S Y)

theorem

surjective_projectionImageSectionMap

L90 ↗

ProCGroups.InverseSystems.surjective_projectionImageSectionMap

Documentation

Each coordinate section map onto a projection image is surjective.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

theorem surjective_projectionImageSectionMap {I : Type u} [Preorder I]
    (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :
    Function.Surjective (projectionImageSectionMap S Y i)

def

projectionImageLift

L104 ↗

ProCGroups.InverseSystems.projectionImageLift

Documentation

The canonical lift from a subset of an inverse limit to the inverse limit of its projection-image system.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

def projectionImageLift {I : Type u} [Preorder I]
    (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
    Y → (S.projectionImageSystem Y).inverseLimit

theorem

continuous_projectionImageLift

L113 ↗

ProCGroups.InverseSystems.continuous_projectionImageLift

Documentation

The lift from a closed subspace into the inverse limit of its projection images is continuous.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

theorem continuous_projectionImageLift {I : Type u} [Preorder I]
    (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
    Continuous (projectionImageLift S Y)

theorem

surjective_projectionImageLift

L123 ↗

ProCGroups.InverseSystems.surjective_projectionImageLift

Documentation

For a closed subset of a compact Hausdorff inverse limit, the canonical projection-image lift is surjective.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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)

theorem

projectionImageLift_comp_subtype

L140 ↗

ProCGroups.InverseSystems.projectionImageLift_comp_subtype

Documentation

Composing the projection-image lift with the inclusion morphism recovers the underlying point of the original inverse limit.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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.val

theorem

surjective_projectionImageSystem_map

L158 ↗

ProCGroups.InverseSystems.InverseSystem.surjective_projectionImageSystem_map

Documentation

The transition maps in the projection-image system are always surjective.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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)

def

homeomorph_projectionImageSystem_of_isClosed

L174 ↗

ProCGroups.InverseSystems.InverseSystem.homeomorph_projectionImageSystem_of_isClosed

Documentation

A closed subset of an inverse limit is homeomorphic to the inverse limit of its projection-image system.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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

theorem

range_limMap_projectionImageInclusion_eq

L203 ↗

ProCGroups.InverseSystems.range_limMap_projectionImageInclusion_eq

Documentation

The range of the limit map is exactly the compatible inverse limit of the projection images.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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)) = Y

theorem

mem_isClosed_iff_forall_projection_mem

L228 ↗

ProCGroups.InverseSystems.InverseSystem.mem_isClosed_iff_forall_projection_mem

Documentation

Membership in the projected image system can be checked coordinatewise.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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 '' Y

theorem

exists_homeomorph_closed_subspace_projection_images

L267 ↗

ProCGroups.InverseSystems.InverseSystem.exists_homeomorph_closed_subspace_projection_images

Documentation

A closed subspace of an inverse limit is again an inverse limit of its projection images.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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)

theorem

projection_image_closure_eq_closure_projection_image

L280 ↗

ProCGroups.InverseSystems.InverseSystem.projection_image_closure_eq_closure_projection_image

Documentation

The projection of the closure of a subset equals the closure of the projection image.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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)

theorem

exists_homeomorph_closure_projection_images

L298 ↗

ProCGroups.InverseSystems.InverseSystem.exists_homeomorph_closure_projection_images

Documentation

The closure of a subset of an inverse limit is homeomorphic to the inverse limit of the projection-image system of that closure.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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)

theorem

closure_eq_of_projection_images_eq

L311 ↗

ProCGroups.InverseSystems.InverseSystem.closure_eq_of_projection_images_eq

Documentation

Closed subsets of the inverse limit are equal when their projection images agree at every stage.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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'

theorem

closure_eq_of_projection_images_eq_of_subsets

L337 ↗

ProCGroups.InverseSystems.InverseSystem.closure_eq_of_projection_images_eq_of_subsets

Documentation

Equal raw projection images of two subsets force their closures in the inverse limit to be equal.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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'

def

homeomorph_surjectiveProjectionImageSystem

L358 ↗

ProCGroups.InverseSystems.InverseSystem.homeomorph_surjectiveProjectionImageSystem

Documentation

Any inverse system of compact Hausdorff spaces admits a surjective projection-image system with the same inverse limit.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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

theorem

exists_homeomorph_surjectiveProjectionImageSystem

L370 ↗

ProCGroups.InverseSystems.InverseSystem.exists_homeomorph_surjectiveProjectionImageSystem

Documentation

The projection-image system of the full inverse limit is surjective and has the same inverse limit as the original system.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w

Lean source · statement

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)

Module documentation

Inverse systems formed from projection images

Declarations