Module

CompatibilityAndSurjectivity.lean

Nyll.ProCGroups.InverseSystems.CompatibilityAndSurjectivity

24 declarations indexed from sourceView source ↗

Module documentation

Morphisms of inverse systems and maps on their limits

Compactness gives nonemptiness of directed inverse limits of nonempty Hausdorff stages. This module then defines continuous stagewise morphisms, constructs their induced maps on inverse limits, and gives stagewise hypotheses ensuring that those maps are injective, embeddings, or surjective.

Imports2

Imported by7

def

CompatibleUpTo

L40 ↗

ProCGroups.InverseSystems.InverseSystem.CompatibleUpTo

Documentation

Compatibility restricted to indices below a fixed stage ensures nonemptiness of the inverse limit.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

def CompatibleUpTo (j : I) (x : ∀ i, S.X i) : Prop

theorem

isClosed_setOf_compatibleUpTo

L47 ↗

ProCGroups.InverseSystems.InverseSystem.isClosed_setOf_compatibleUpTo

Documentation

For a fixed stage j, the product families whose earlier coordinates are determined by their j-coordinate form a closed subset when all stages are Hausdorff.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem isClosed_setOf_compatibleUpTo [∀ i, T2Space (S.X i)] (j : I) :
    IsClosed {x : ∀ i, S.X i | S.CompatibleUpTo j x}

theorem

compatibleUpTo_nonempty

L57 ↗

ProCGroups.InverseSystems.InverseSystem.compatibleUpTo_nonempty

Documentation

A point at stage j, transported to every earlier stage and completed arbitrarily elsewhere, gives a family compatible up to j.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem compatibleUpTo_nonempty (j : I) [∀ i, Nonempty (S.X i)] :
    ({x : ∀ i, S.X i | S.CompatibleUpTo j x} : Set (∀ i, S.X i)).Nonempty

theorem

compatibleUpTo_mono

L68 ↗

ProCGroups.InverseSystems.InverseSystem.compatibleUpTo_mono

Documentation

Compatibility up to a later stage implies compatibility up to every earlier stage.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem compatibleUpTo_mono {j j' : I} (hjj' : j ≤ j') :
    {x : ∀ i, S.X i | S.CompatibleUpTo j' x} ⊆ {x : ∀ i, S.X i | S.CompatibleUpTo j x}

theorem

nonempty_inverseLimit

L77 ↗

ProCGroups.InverseSystems.InverseSystem.nonempty_inverseLimit

Documentation

The inverse limit of nonempty compact Hausdorff spaces is nonempty.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem nonempty_inverseLimit [∀ i, Nonempty (S.X i)] [∀ i, CompactSpace (S.X i)]
    [∀ i, T2Space (S.X i)] (hdir : Directed (· ≤ ·) (id : I → I)) :
    Nonempty S.inverseLimit

theorem

nonempty_inverseLimit_of_finite

L102 ↗

ProCGroups.InverseSystems.InverseSystem.nonempty_inverseLimit_of_finite

Documentation

Special case for inverse systems of nonempty finite discrete spaces.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem nonempty_inverseLimit_of_finite [∀ i, Finite (S.X i)] [∀ i, Nonempty (S.X i)]
    [∀ i, DiscreteTopology (S.X i)] (hdir : Directed (· ≤ ·) (id : I → I)) :
    Nonempty S.inverseLimit

structure

Morphism

L108 ↗

ProCGroups.InverseSystems.InverseSystem.Morphism

Documentation

A morphism of inverse systems over the same directed preorder.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · full declaration

structure Morphism (T : InverseSystem (I := I)) where
  /-- The map from the source stage to the target stage at each index. -/
  map : ∀ i, S.X i → T.X i
  /-- Every stage map is continuous. -/
  continuous_map : ∀ i, Continuous (map i)
  /-- The stage maps form a natural transformation: they commute with all transition maps. -/
  comm : ∀ {i j : I} (hij : i ≤ j), T.map hij ∘ map j = map i ∘ S.map hij

theorem

comm_apply

L122 ↗

ProCGroups.InverseSystems.InverseSystem.Morphism.comm_apply

Documentation

A morphism of inverse systems commutes pointwise with transition maps.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
namespace Morphism
variable {S}
variable {T U : InverseSystem (I := I)}

Lean source · statement

theorem comm_apply (Θ : S.Morphism T) {i j : I} (hij : i ≤ j) (x : S.X j) :
    T.map hij (Θ.map j x) = Θ.map i (S.map hij x)

def

id

L127 ↗

ProCGroups.InverseSystems.InverseSystem.Morphism.id

Documentation

The identity morphism of an inverse system.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
namespace Morphism
variable {S}
variable {T U : InverseSystem (I := I)}

Lean source · full declaration

def id (S : InverseSystem (I := I)) : S.Morphism S where
  map := fun _ => fun x => x
  continuous_map := fun _ => continuous_id
  comm := fun _ => by
    funext x
    rfl

theorem

id_apply

L135 ↗

ProCGroups.InverseSystems.InverseSystem.Morphism.id_apply

Documentation

The identity morphism of an inverse system acts as the identity at each stage.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
namespace Morphism
variable {S}
variable {T U : InverseSystem (I := I)}

Lean source · statement

theorem id_apply (i : I) (x : S.X i) :
    (id S).map i x = x

def

comp

L139 ↗

ProCGroups.InverseSystems.InverseSystem.Morphism.comp

Documentation

Morphisms of inverse systems compose stagewise.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
namespace Morphism
variable {S}
variable {T U : InverseSystem (I := I)}

Lean source · full declaration

def comp (Φ : T.Morphism U) (Θ : S.Morphism T) : S.Morphism U where
  map := fun i => Φ.map i ∘ Θ.map i
  continuous_map := fun i => (Φ.continuous_map i).comp (Θ.continuous_map i)
  comm := fun {i j} hij => by
    funext x
    calc
      U.map hij ((Φ.map j ∘ Θ.map j) x) = U.map hij (Φ.map j (Θ.map j x)) := rfl
      _ = Φ.map i (T.map hij (Θ.map j x)) := by
        exact congrFun (Φ.comm hij) (Θ.map j x)
      _ = Φ.map i (Θ.map i (S.map hij x)) := by
        rw [Θ.comm_apply hij x]
      _ = ((Φ.map i ∘ Θ.map i) ∘ S.map hij) x := by
        rfl

theorem

comp_apply

L154 ↗

ProCGroups.InverseSystems.InverseSystem.Morphism.comp_apply

Documentation

At stage i, the composite morphism applies the stage map of Θ followed by that of Φ.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
namespace Morphism
variable {S}
variable {T U : InverseSystem (I := I)}

Lean source · statement

theorem comp_apply (Φ : T.Morphism U) (Θ : S.Morphism T) (i : I) (x : S.X i) :
    (comp Φ Θ).map i x = Φ.map i (Θ.map i x)

theorem

compatibleMaps_morphism

L160 ↗

ProCGroups.InverseSystems.InverseSystem.compatibleMaps_morphism

Documentation

A morphism of inverse systems sends inverse-limit projections to a compatible family.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · full declaration

theorem compatibleMaps_morphism {T : InverseSystem (I := I)} (Θ : S.Morphism T) :
    T.CompatibleMaps (fun i => Θ.map i ∘ S.projection i) := by
  intro i j hij
  funext x
  calc
    T.map hij (Θ.map j (S.projection j x)) = Θ.map i (S.map hij (S.projection j x)) := by
      exact Θ.comm_apply hij (S.projection j x)
    _ = Θ.map i (S.projection i x) := by rw [S.projection_compatible x i j hij]

def

limMap

L170 ↗

ProCGroups.InverseSystems.InverseSystem.limMap

Documentation

A morphism of inverse systems induces a map on inverse limits.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

def limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T) :
    S.inverseLimit → T.inverseLimit

theorem

π_comp_limMap

L175 ↗

ProCGroups.InverseSystems.InverseSystem.π_comp_limMap

Documentation

Projection after the inverse-system limit map agrees with the corresponding stage map.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem π_comp_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T) (i : I) :
    T.projection i ∘ S.limMap Θ = Θ.map i ∘ S.projection i

theorem

π_limMap_apply

L183 ↗

ProCGroups.InverseSystems.InverseSystem.π_limMap_apply

Documentation

Projecting the induced map on inverse limits to stage \(i\) gives the corresponding stage map after projection.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem π_limMap_apply {T : InverseSystem (I := I)} (Θ : S.Morphism T)
    (i : I) (x : S.inverseLimit) :
    T.projection i (S.limMap Θ x) = Θ.map i (S.projection i x)

theorem

continuous_limMap

L192 ↗

ProCGroups.InverseSystems.InverseSystem.continuous_limMap

Documentation

A projection after the induced map on inverse limits is the corresponding stage map after projection.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem continuous_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T) :
    Continuous (S.limMap Θ)

theorem

limMap_id

L200 ↗

ProCGroups.InverseSystems.InverseSystem.limMap_id

Documentation

The inverse-limit map induced by the identity morphism is the identity.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem limMap_id :
    S.limMap (Morphism.id S) = id

theorem

limMap_comp

L210 ↗

ProCGroups.InverseSystems.InverseSystem.limMap_comp

Documentation

The inverse-limit map induced by a composite morphism is the composite of the induced maps.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem limMap_comp {T U : InverseSystem (I := I)} (Φ : T.Morphism U) (Θ : S.Morphism T) :
    S.limMap (Morphism.comp Φ Θ) = T.limMap Φ ∘ S.limMap Θ

theorem

injective_limMap

L224 ↗

ProCGroups.InverseSystems.InverseSystem.injective_limMap

Documentation

The induced map on inverse limits is injective when all stage maps are injective.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem injective_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T)
    (hinj : ∀ i, Function.Injective (Θ.map i)) :
    Function.Injective (S.limMap Θ)

theorem

embedding_limMap

L243 ↗

ProCGroups.InverseSystems.InverseSystem.embedding_limMap

Documentation

If all components of a morphism of inverse systems are embeddings, then the induced map on inverse limits is an embedding.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem embedding_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T)
    (hemb : ∀ i, Topology.IsEmbedding (Θ.map i)) :
    Topology.IsEmbedding (S.limMap Θ)

theorem

surjective_limMap

L268 ↗

ProCGroups.InverseSystems.InverseSystem.surjective_limMap

Documentation

If all components of a morphism of inverse systems are surjective, then the induced map on inverse limits is surjective.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem surjective_limMap {T : InverseSystem (I := I)} [∀ i, CompactSpace (S.X i)]
    [∀ i, T2Space (S.X i)] [∀ i, T2Space (T.X i)] (hdir : Directed (· ≤ ·) (id : I → I))
    (Θ : S.Morphism T) (hsurj : ∀ i, Function.Surjective (Θ.map i)) :
    Function.Surjective (S.limMap Θ)

theorem

surjective_inverseLimitLift

L324 ↗

ProCGroups.InverseSystems.InverseSystem.surjective_inverseLimitLift

Documentation

Compatible surjections from a compact space induce a surjection onto the inverse limit.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem surjective_inverseLimitLift {X : Type w} [TopologicalSpace X] [CompactSpace X]
    [Nonempty I]
    (ψ : ∀ i, X → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
    (hsurj : ∀ i, Function.Surjective (ψ i)) (hdir : Directed (· ≤ ·) (id : I → I))
    [∀ i, T2Space (S.X i)] :
    Function.Surjective (S.inverseLimitLift ψ hcompat)

theorem

exists_injective_projection_of_finite_inverseLimit

L362 ↗

ProCGroups.InverseSystems.InverseSystem.exists_injective_projection_of_finite_inverseLimit

Documentation

If an inverse limit over a directed index set is finite, one projection separates all points.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))

Lean source · statement

theorem exists_injective_projection_of_finite_inverseLimit [Nonempty I]
    (hdir : Directed (· ≤ ·) (id : I → I)) [Finite S.inverseLimit] :
    ∃ k, Function.Injective (S.projection k)

Module documentation

Morphisms of inverse systems and maps on their limits

Declarations