NYLL
Module

Basic.lean

Nyll.ProCGroups.InverseSystems.Basic
91 declarations indexed from sourceView source ↗

Module documentation

Concrete inverse systems and their limits

This module defines preorder-indexed inverse systems of topological spaces and realizes their inverse limit as the subtype of compatible families. It proves the topological universal property and equips limits of group, additive-group, module, and ring systems with their coordinatewise algebraic structures and canonical projection homomorphisms.

Imports2
  • Mathlib.Topology.Algebra.Ring.Basic
  • Mathlib.Algebra.Module.Pi
Imported by10

Declarations

structure

InverseSystem

L33 ↗
ProCGroups.InverseSystems.InverseSystem
Documentation

An inverse system of topological spaces indexed by a preorder.

Source context 7 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
Lean source · full declaration
structure InverseSystem where
  /-- The topological space assigned to each index of the system. -/
  X : I → Type v
  /-- The chosen topology on every stage; this field supplies the stagewise topology instance. -/
  topologicalSpace : ∀ i, TopologicalSpace (X i)
  /-- The contravariant transition map from stage `j` to stage `i` whenever `i ≤ j`. -/
  map : ∀ {i j : I}, i ≤ j → X j → X i
  /-- Every transition map is continuous for the chosen stage topologies. -/
  continuous_map : ∀ {i j : I} (hij : i ≤ j), Continuous (map hij)
  /-- Transition along a reflexive comparison is the identity map. -/
  map_id : ∀ i, map (le_rfl : i ≤ i) = id
  /-- Transition maps compose according to transitivity of the indexing preorder. -/
  map_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
    map hij ∘ map hjk = map (hij.trans hjk)
theorem

map_id_apply

L55 ↗
ProCGroups.InverseSystems.InverseSystem.map_id_apply
Documentation

The transition map along \(i \le i\) is the identity on points.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem map_id_apply (i : I) (x : S.X i) :
    S.map (le_rfl : i ≤ i) x = x
theorem

map_comp_apply

L63 ↗
ProCGroups.InverseSystems.InverseSystem.map_comp_apply
Documentation

Following the transition from k to j by the transition from j to i agrees pointwise with the direct transition from k to i.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem map_comp_apply {i j k : I} (hij : i ≤ j) (hjk : j ≤ k) (x : S.X k) :
    S.map hij (S.map hjk x) = S.map (hij.trans hjk) x
def

Compatible

L68 ↗
ProCGroups.InverseSystems.InverseSystem.Compatible
Documentation

Compatibility of a family of points in the product.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
def Compatible (x : ∀ i, S.X i) : Prop
def

CompatibleMaps

L72 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleMaps
Documentation

Compatibility of a family of maps into an inverse system.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
def CompatibleMaps {Y : Type w} (ψ : ∀ i, Y → S.X i) : Prop
abbrev

inverseLimit

L76 ↗
ProCGroups.InverseSystems.InverseSystem.inverseLimit
Documentation

The inverse limit realized as a subtype of the product.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
abbrev inverseLimit : Type _
def

projection

L79 ↗
ProCGroups.InverseSystems.InverseSystem.projection
Documentation

The canonical projection from the inverse limit to the \(i\)-th component.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
def projection (i : I) : S.inverseLimit → S.X i
def

IsLinearSystem

L86 ↗
ProCGroups.InverseSystems.InverseSystem.IsLinearSystem
Documentation

Linearity data for an inverse system and its concrete inverse-limit cone. This companion predicate packages the scalar-compatibility facts used by Hom-comparison formulations, without installing them as global typeclass instances.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
def IsLinearSystem {R : Type w} [Semiring R] (S : InverseSystem (I := I))
    [∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
    [AddCommMonoid S.inverseLimit] [Module R S.inverseLimit] : Prop
theorem

map_smul

L96 ↗
ProCGroups.InverseSystems.InverseSystem.IsLinearSystem.map_smul
Documentation

Maps in a linear inverse system commute with scalar multiplication.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsLinearSystem
Lean source · statement
theorem map_smul {R : Type w} [Semiring R] {S : InverseSystem (I := I)}
    [∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
    [AddCommMonoid S.inverseLimit] [Module R S.inverseLimit]
    (hS : IsLinearSystem (R := R) S) {i j : I} (hij : i ≤ j) (r : R) (x : S.X j) :
    S.map hij (r • x) = r • S.map hij x
theorem

projection_smul

L104 ↗
ProCGroups.InverseSystems.InverseSystem.IsLinearSystem.projection_smul
Documentation

The finite-stage projection commutes with scalar multiplication by coefficients.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsLinearSystem
Lean source · statement
theorem projection_smul {R : Type w} [Semiring R] {S : InverseSystem (I := I)}
    [∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
    [AddCommMonoid S.inverseLimit] [Module R S.inverseLimit]
    (hS : IsLinearSystem (R := R) S) (i : I) (r : R) (x : S.inverseLimit) :
    S.projection i (r • x) = r • S.projection i x
theorem

projection_apply

L114 ↗
ProCGroups.InverseSystems.InverseSystem.projection_apply
Documentation

Applying a projection to an inverse-limit element returns its corresponding stage coordinate.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem projection_apply (i : I) (x : S.inverseLimit) :
    S.projection i x = x.1 i
theorem

projection_compatible

L118 ↗
ProCGroups.InverseSystems.InverseSystem.projection_compatible
Documentation

Projections from the inverse limit are compatible with the transition maps.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem projection_compatible (x : S.inverseLimit) (i j : I) (hij : i ≤ j) :
    S.map hij (S.projection j x) = S.projection i x
theorem

projection_compatibleMaps

L123 ↗
ProCGroups.InverseSystems.InverseSystem.projection_compatibleMaps
Documentation

The canonical projections form a compatible family of maps.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem projection_compatibleMaps : S.CompatibleMaps S.projection
theorem

continuous_projection

L129 ↗
ProCGroups.InverseSystems.InverseSystem.continuous_projection
Documentation

Each canonical projection from an inverse limit is continuous.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem continuous_projection (i : I) : Continuous (S.projection i)
theorem

ext

L133 ↗
ProCGroups.InverseSystems.InverseSystem.ext
Documentation

Two inverse-limit points are equal when all their projections are equal.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem ext {x y : S.inverseLimit}
    (h : ∀ i, S.projection i x = S.projection i y) : x = y
def

inverseLimitLift

L140 ↗
ProCGroups.InverseSystems.InverseSystem.inverseLimitLift
Documentation

The concrete map induced by a compatible family of maps into the subtype inverse limit.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
def inverseLimitLift {Y : Type w} (ψ : ∀ i, Y → S.X i)
    (hcompat : S.CompatibleMaps ψ) :
    Y → S.inverseLimit
theorem

projection_comp_inverseLimitLift

L148 ↗
ProCGroups.InverseSystems.InverseSystem.projection_comp_inverseLimitLift
Documentation

Composing a canonical projection with the lift recovers the corresponding compatible map.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem projection_comp_inverseLimitLift {Y : Type w} (ψ : ∀ i, Y → S.X i)
    (hcompat : S.CompatibleMaps ψ) (i : I) :
    S.projection i ∘ S.inverseLimitLift ψ hcompat = ψ i
theorem

projection_inverseLimitLift_apply

L153 ↗
ProCGroups.InverseSystems.InverseSystem.projection_inverseLimitLift_apply
Documentation

Applying a projection to an inverse-limit lift returns the corresponding stage map value.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem projection_inverseLimitLift_apply {Y : Type w} (ψ : ∀ i, Y → S.X i)
    (hcompat : S.CompatibleMaps ψ) (i : I) (y : Y) :
    S.projection i (S.inverseLimitLift ψ hcompat y) = ψ i y
theorem

inverseLimitLift_unique

L158 ↗
ProCGroups.InverseSystems.InverseSystem.inverseLimitLift_unique
Documentation

A map into the subtype inverse limit is uniquely determined by its projections.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem inverseLimitLift_unique {Y : Type w} (ψ : ∀ i, Y → S.X i)
    (hcompat : S.CompatibleMaps ψ) {f : Y → S.inverseLimit}
    (hf : ∀ i, S.projection i ∘ f = ψ i) :
    f = S.inverseLimitLift ψ hcompat
theorem

continuous_inverseLimitLift

L170 ↗
ProCGroups.InverseSystems.InverseSystem.continuous_inverseLimitLift
Documentation

A lift from a topological space is continuous when all of its component maps are continuous.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem continuous_inverseLimitLift {Y : Type w} [TopologicalSpace Y] (ψ : ∀ i, Y → S.X i)
    (hψ : ∀ i, Continuous (ψ i))
    (hcompat : S.CompatibleMaps ψ) :
    Continuous (S.inverseLimitLift ψ hcompat)
structure

IsInverseLimit

L179 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit
Documentation

The universal property of an inverse limit.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · full declaration
structure IsInverseLimit {L : Type w} [TopologicalSpace L] (π : ∀ i, L → S.X i) : Prop where
  /-- Each leg of the proposed limiting cone is continuous. -/
  continuous_proj : ∀ i, Continuous (π i)
  /-- The cone legs commute with every transition map of the inverse system. -/
  compatible : S.CompatibleMaps π
  /--
  Every continuous compatible cone, including one in the designated larger source universe,
  factors through `L` by a unique continuous map.
  -/
  existsUnique_lift :
    ∀ {Y : Type max u v w} [TopologicalSpace Y] (ψ : ∀ i, Y → S.X i)
      (_hψ : ∀ i, Continuous (ψ i)) (_hcompat : S.CompatibleMaps ψ),
      ∃! f : Y → L, Continuous f ∧ ∀ i, π i ∘ f = ψ i
theorem

existsUnique_lift_sameUniverse

L201 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.existsUnique_lift_sameUniverse
Documentation

The large-universe universal property induces the usual universal property for sources in the carrier universe. The ULift is essential: universe levels cannot themselves be quantified inside a structure field.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
theorem existsUnique_lift_sameUniverse (hπ : S.IsInverseLimit π)
    {Y : Type w} [TopologicalSpace Y]
    (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i))
    (hcompat : S.CompatibleMaps ψ) :
    ∃! f : Y → L, Continuous f ∧ ∀ i, π i ∘ f = ψ i
def

lift

L233 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.lift
Documentation

A compatible family of maps to the stages lifts uniquely to a map into the inverse limit.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
def lift (hπ : S.IsInverseLimit π)
    {Y : Type w} [TopologicalSpace Y]
    (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
    Y → L
theorem

lift_spec

L241 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.lift_spec
Documentation

The universal-property lift is continuous and has the prescribed projections.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
theorem lift_spec (hπ : S.IsInverseLimit π)
    {Y : Type w} [TopologicalSpace Y]
    (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
    Continuous (hπ.lift ψ hψ hcompat) ∧
      ∀ i, π i ∘ hπ.lift ψ hψ hcompat = ψ i
theorem

continuous_lift

L250 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.continuous_lift
Documentation

The lift into the inverse limit is continuous when all coordinate maps are continuous.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
theorem continuous_lift (hπ : S.IsInverseLimit π)
    {Y : Type w} [TopologicalSpace Y]
    (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
    Continuous (hπ.lift ψ hψ hcompat)
theorem

fac

L257 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.fac
Documentation

The universal-property lift has the prescribed i-th projection.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
theorem fac (hπ : S.IsInverseLimit π)
    {Y : Type w} [TopologicalSpace Y]
    (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
    (i : I) :
    π i ∘ hπ.lift ψ hψ hcompat = ψ i
theorem

uniq

L265 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.uniq
Documentation

The universal-property lift is the unique continuous map with the prescribed projections.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
theorem uniq (hπ : S.IsInverseLimit π)
    {Y : Type w} [TopologicalSpace Y]
    (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
    {f : Y → L} (hf : Continuous f) (hfac : ∀ i, π i ∘ f = ψ i) :
    f = hπ.lift ψ hψ hcompat
theorem

lift_self

L274 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.lift_self
Documentation

Lifting the projection family of an inverse limit gives the identity map.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
theorem lift_self (hπ : S.IsInverseLimit π) :
    hπ.lift (Y := L) π hπ.continuous_proj hπ.compatible = id
theorem

existsUnique_lift_from_inverseLimit

L281 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.existsUnique_lift_from_inverseLimit
Documentation

The large-universe universal property also supplies the comparison map from the concrete compatible-family model; this is a theorem, not duplicate structure data.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
theorem existsUnique_lift_from_inverseLimit (hπ : S.IsInverseLimit π) :
    ∃! f : S.inverseLimit → L,
      Continuous f ∧ ∀ i, π i ∘ f = S.projection i
def

liftFromInverseLimit

L312 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.liftFromInverseLimit
Documentation

The lift from the concrete compatible-family inverse limit.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
def liftFromInverseLimit (hπ : S.IsInverseLimit π) :
    S.inverseLimit → L
theorem

liftFromInverseLimit_spec

L317 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.liftFromInverseLimit_spec
Documentation

The concrete inverse-limit lift is continuous and has the prescribed projections.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
theorem liftFromInverseLimit_spec (hπ : S.IsInverseLimit π) :
    Continuous hπ.liftFromInverseLimit ∧
      ∀ i, π i ∘ hπ.liftFromInverseLimit = S.projection i
def

homeomorphToInverseLimit

L325 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.homeomorphToInverseLimit
Documentation

Every abstract inverse-limit cone is canonically homeomorphic to the concrete compatible-family model. Factoring comparison through this model makes the construction independent of the carrier's universe.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · full declaration
def homeomorphToInverseLimit (hπ : S.IsInverseLimit π) :
    L ≃ₜ S.inverseLimit where
  toFun := S.inverseLimitLift π hπ.compatible
  invFun := hπ.liftFromInverseLimit
  left_inv := by
    intro x
    let f : L → S.inverseLimit := S.inverseLimitLift π hπ.compatible
    let g : S.inverseLimit → L := hπ.liftFromInverseLimit
    have hgf : g ∘ f = id := by
      exact (hπ.existsUnique_lift_sameUniverse π hπ.continuous_proj hπ.compatible).unique
        (by
          refine ⟨hπ.liftFromInverseLimit_spec.1.comp
            (S.continuous_inverseLimitLift π hπ.continuous_proj hπ.compatible), ?_⟩
          intro i
          calc
            π i ∘ (g ∘ f) = (π i ∘ g) ∘ f := by rfl
            _ = S.projection i ∘ f := by
              rw [hπ.liftFromInverseLimit_spec.2 i]
            _ = π i := S.projection_comp_inverseLimitLift π hπ.compatible i)
        ⟨continuous_id, fun _ => rfl⟩
    exact congrFun hgf x
  right_inv := by
    intro x
    apply S.ext
    intro i
    rw [S.projection_inverseLimitLift_apply]
    exact congrFun
      (hπ.liftFromInverseLimit_spec.2 i) x
  continuous_toFun :=
    S.continuous_inverseLimitLift π hπ.continuous_proj hπ.compatible
  continuous_invFun := hπ.liftFromInverseLimit_spec.1
def

homeomorph

L358 ↗
ProCGroups.InverseSystems.InverseSystem.IsInverseLimit.homeomorph
Documentation

Inverse limits are unique up to unique homeomorphism.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
namespace IsInverseLimit
variable {S : InverseSystem.{u, v} (I := I)}
variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
Lean source · statement
def homeomorph {L' : Type z} [TopologicalSpace L'] {π' : ∀ i, L' → S.X i}
    (hπ : S.IsInverseLimit π) (hπ' : S.IsInverseLimit π') :
    L ≃ₜ L'
theorem

isInverseLimit_projection

L366 ↗
ProCGroups.InverseSystems.InverseSystem.isInverseLimit_projection
Documentation

The subtype model carries the inverse-limit universal property.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem isInverseLimit_projection : S.IsInverseLimit S.projection
theorem

isClosed_setOf_compatible

L376 ↗
ProCGroups.InverseSystems.InverseSystem.isClosed_setOf_compatible
Documentation

The inverse limit is a closed subspace of the product.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem isClosed_setOf_compatible [∀ i, T2Space (S.X i)] :
    IsClosed {x : ∀ i, S.X i | S.Compatible x}
instance

instCompactSpaceInverseLimit

L386 ↗
ProCGroups.InverseSystems.InverseSystem.instCompactSpaceInverseLimit
Documentation

The constructed object carries the compact space structure inherited from its profinite construction.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
instance instCompactSpaceInverseLimit [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)] :
    CompactSpace S.inverseLimit
theorem

t2Space_inverseLimit

L392 ↗
ProCGroups.InverseSystems.InverseSystem.t2Space_inverseLimit
Documentation

Inverse limits of Hausdorff spaces are Hausdorff.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem t2Space_inverseLimit [∀ i, T2Space (S.X i)] :
    T2Space S.inverseLimit
theorem

totallyDisconnectedSpace_inverseLimit

L396 ↗
ProCGroups.InverseSystems.InverseSystem.totallyDisconnectedSpace_inverseLimit
Documentation

Inverse limits of totally disconnected spaces are totally disconnected.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem totallyDisconnectedSpace_inverseLimit [∀ i, TotallyDisconnectedSpace (S.X i)] :
    TotallyDisconnectedSpace S.inverseLimit
theorem

isQuotientMap_projection_of_surjective

L400 ↗
ProCGroups.InverseSystems.InverseSystem.isQuotientMap_projection_of_surjective
Documentation

A surjective projection from a compact inverse limit to a Hausdorff stage is a quotient map.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem.{u, v} (I := I))
Lean source · statement
theorem isQuotientMap_projection_of_surjective [∀ i, CompactSpace (S.X i)]
    [∀ i, T2Space (S.X i)] {i : I} (hsurj : Function.Surjective (S.projection i)) :
    Topology.IsQuotientMap (S.projection i)
class

IsGroupSystem

L412 ↗
ProCGroups.InverseSystems.IsGroupSystem
Documentation

A group-valued inverse system whose transition maps are group homomorphisms.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
Lean source · full declaration
class IsGroupSystem (S : InverseSystem (I := I)) [∀ i, Group (S.X i)] : Prop where
  /-- Transition maps preserve the identity element at every pair of comparable stages. -/
  map_one : ∀ {i j : I} (hij : i ≤ j), S.map hij 1 = 1
  /-- Transition maps preserve products at every pair of comparable stages. -/
  map_mul : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
    S.map hij (x * y) = S.map hij x * S.map hij y
  /-- Transition maps preserve inverses at every pair of comparable stages. -/
  map_inv : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
    S.map hij x⁻¹ = (S.map hij x)⁻¹
instance

instOneInverseLimit

L425 ↗
ProCGroups.InverseSystems.instOneInverseLimit
Documentation

The unit of the inverse limit is the compatible family of units at all stages.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · full declaration
instance instOneInverseLimit : One S.inverseLimit where
  one := ⟨fun i => 1, by
    intro i j hij
    simpa using IsGroupSystem.map_one (S := S) hij⟩
instance

instMulInverseLimit

L433 ↗
ProCGroups.InverseSystems.instMulInverseLimit
Documentation

Multiplication on the inverse limit is defined coordinatewise through the stage multiplications.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · full declaration
instance instMulInverseLimit : Mul S.inverseLimit where
  mul x y := ⟨fun i => S.projection i x * S.projection i y, by
    intro i j hij
    calc
      S.map hij (S.projection j x * S.projection j y)
          = S.map hij (S.projection j x) * S.map hij (S.projection j y) := by
              simpa using IsGroupSystem.map_mul (S := S) hij (S.projection j x)
                (S.projection j y)
      _ = S.projection i x * S.projection i y := by
          rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩
instance

instInvInverseLimit

L445 ↗
ProCGroups.InverseSystems.instInvInverseLimit
Documentation

The inverse-limit object carries the structure induced coordinatewise from the finite stages.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · full declaration
instance instInvInverseLimit : Inv S.inverseLimit where
  inv x := ⟨fun i => (S.projection i x)⁻¹, by
    intro i j hij
    calc
      S.map hij ((S.projection j x)⁻¹) = (S.map hij (S.projection j x))⁻¹ := by
        simpa using IsGroupSystem.map_inv (S := S) hij (S.projection j x)
      _ = (S.projection i x)⁻¹ := by rw [S.projection_compatible x i j hij]⟩
theorem

projection_one

L454 ↗
ProCGroups.InverseSystems.projection_one
Documentation

The projection of the identity element is the identity at each stage.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · statement
theorem projection_one (i : I) : S.projection i (1 : S.inverseLimit) = 1
theorem

projection_mul

L457 ↗
ProCGroups.InverseSystems.projection_mul
Documentation

Projection commutes with multiplication in a group-valued inverse system.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · statement
theorem projection_mul (i : I) (x y : S.inverseLimit) :
    S.projection i (x * y) = S.projection i x * S.projection i y
theorem

projection_inv

L461 ↗
ProCGroups.InverseSystems.projection_inv
Documentation

Projection commutes with inversion in a group-valued inverse system.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · statement
theorem projection_inv (i : I) (x : S.inverseLimit) :
    S.projection i x⁻¹ = (S.projection i x)⁻¹
instance

instGroupInverseLimit

L468 ↗
ProCGroups.InverseSystems.instGroupInverseLimit
Documentation

The constructed carrier inherits its group structure from the coordinatewise group structure of the construction.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · full declaration
instance instGroupInverseLimit : Group S.inverseLimit where
  one := 1
  mul := (· * ·)
  inv := Inv.inv
  mul_assoc x y z := by
    apply S.ext
    intro i
    change ((x.1 i * y.1 i) * z.1 i) = (x.1 i * (y.1 i * z.1 i))
    simp only [mul_assoc]
  one_mul x := by
    apply S.ext
    intro i
    change 1 * x.1 i = x.1 i
    simp only [one_mul]
  mul_one x := by
    apply S.ext
    intro i
    change x.1 i * 1 = x.1 i
    simp only [mul_one]
  inv_mul_cancel x := by
    apply S.ext
    intro i
    change (x.1 i)⁻¹ * x.1 i = 1
    simp only [inv_mul_cancel]
instance

instIsTopologicalGroupInverseLimit

L494 ↗
ProCGroups.InverseSystems.instIsTopologicalGroupInverseLimit
Documentation

The object is a topological group with the induced group operations and topology.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · full declaration
instance instIsTopologicalGroupInverseLimit [∀ i, IsTopologicalGroup (S.X i)] :
    IsTopologicalGroup S.inverseLimit where
  continuous_mul := by
    exact Continuous.subtype_mk
      (continuous_pi fun i =>
        ((S.continuous_projection i).comp continuous_fst).mul
          ((S.continuous_projection i).comp continuous_snd))
      (fun xy => by
        intro i j hij
        change S.map hij (S.projection j xy.1 * S.projection j xy.2) =
          S.projection i xy.1 * S.projection i xy.2
        rw [IsGroupSystem.map_mul (S := S) hij,
          S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
  continuous_inv := by
    exact Continuous.subtype_mk
      (continuous_pi fun i => continuous_inv.comp (S.continuous_projection i))
      (fun x => by
        intro i j hij
        change S.map hij ((S.projection j x)⁻¹) = (S.projection i x)⁻¹
        rw [IsGroupSystem.map_inv (S := S) hij, S.projection_compatible x i j hij])
def

projectionHom

L516 ↗
ProCGroups.InverseSystems.projectionHom
Documentation

The canonical projections from a group-valued inverse limit are homomorphisms.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · full declaration
def projectionHom (i : I) : S.inverseLimit →* S.X i where
  toFun := S.projection i
  map_one' := projection_one (S := S) i
  map_mul' := by
    intro x y
    exact projection_mul (S := S) i x y
theorem

projectionHom_apply

L527 ↗
ProCGroups.InverseSystems.projectionHom_apply
Documentation

Applying a homomorphic projection to an inverse-limit element returns its corresponding stage coordinate.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section GroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · statement
theorem projectionHom_apply (i : I) (x : S.inverseLimit) :
    projectionHom (S := S) i x = S.projection i x
class

IsAddGroupSystem

L537 ↗
ProCGroups.InverseSystems.IsAddGroupSystem
Documentation

An additive-group-valued inverse system whose transition maps are additive homomorphisms.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
Lean source · full declaration
class IsAddGroupSystem (S : InverseSystem (I := I)) [∀ i, AddCommGroup (S.X i)] : Prop where
  /-- Transition maps preserve zero at every pair of comparable stages. -/
  map_zero : ∀ {i j : I} (hij : i ≤ j), S.map hij 0 = 0
  /-- Transition maps preserve addition at every pair of comparable stages. -/
  map_add : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
    S.map hij (x + y) = S.map hij x + S.map hij y
  /-- Transition maps preserve additive inverses at every pair of comparable stages. -/
  map_neg : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
    S.map hij (-x) = -S.map hij x
class

IsModuleSystem

L550 ↗
ProCGroups.InverseSystems.IsModuleSystem
Documentation

A module-valued inverse system whose transition maps are linear over a fixed semiring.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · full declaration
class IsModuleSystem (R : Type w) [Semiring R] (S : InverseSystem (I := I))
    [∀ i, AddCommGroup (S.X i)] [∀ i, Module R (S.X i)] : Prop where
  /-- Transition maps commute with the fixed `R`-scalar action on all stages. -/
  map_smul : ∀ {i j : I} (hij : i ≤ j) (r : R) (x : S.X j),
    S.map hij (r • x) = r • S.map hij x
instance

instZeroAddInverseLimit

L559 ↗
ProCGroups.InverseSystems.instZeroAddInverseLimit
Documentation

The zero element of the inverse limit is the compatible family of zero elements at all stages.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · full declaration
instance instZeroAddInverseLimit : Zero S.inverseLimit where
  zero := ⟨fun i => 0, by
    intro i j hij
    simpa using IsAddGroupSystem.map_zero (S := S) hij⟩
instance

instAddAddInverseLimit

L565 ↗
ProCGroups.InverseSystems.instAddAddInverseLimit
Documentation

Addition in the additive inverse limit is defined coordinatewise.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · full declaration
instance instAddAddInverseLimit : Add S.inverseLimit where
  add x y := ⟨fun i => S.projection i x + S.projection i y, by
    intro i j hij
    calc
      S.map hij (S.projection j x + S.projection j y)
          = S.map hij (S.projection j x) + S.map hij (S.projection j y) := by
              simpa using IsAddGroupSystem.map_add (S := S) hij (S.projection j x)
                (S.projection j y)
      _ = S.projection i x + S.projection i y := by
          rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩
instance

instNegAddInverseLimit

L577 ↗
ProCGroups.InverseSystems.instNegAddInverseLimit
Documentation

Negation on an additive inverse limit is defined coordinatewise through the stage negations.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · full declaration
instance instNegAddInverseLimit : Neg S.inverseLimit where
  neg x := ⟨fun i => -S.projection i x, by
    intro i j hij
    calc
      S.map hij (-S.projection j x) = -S.map hij (S.projection j x) := by
        simpa using IsAddGroupSystem.map_neg (S := S) hij (S.projection j x)
      _ = -S.projection i x := by rw [S.projection_compatible x i j hij]⟩
instance

instSubAddInverseLimit

L586 ↗
ProCGroups.InverseSystems.instSubAddInverseLimit
Documentation

Subtraction in the inverse limit is defined coordinatewise through the stage subtractions.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · full declaration
instance instSubAddInverseLimit : Sub S.inverseLimit where
  sub x y := ⟨fun i => S.projection i x - S.projection i y, by
    intro i j hij
    change S.map hij (S.projection j x - S.projection j y) =
      S.projection i x - S.projection i y
    rw [sub_eq_add_neg, IsAddGroupSystem.map_add, IsAddGroupSystem.map_neg,
      S.projection_compatible x i j hij, S.projection_compatible y i j hij, sub_eq_add_neg]⟩
instance

instSMulNatAddInverseLimit

L595 ↗
ProCGroups.InverseSystems.instSMulNatAddInverseLimit
Documentation

An additive inverse limit carries natural-number scalar multiplication coordinatewise.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · full declaration
instance instSMulNatAddInverseLimit : SMul ℕ S.inverseLimit where
  smul n x := ⟨fun i => n • S.projection i x, by
    intro i j hij
    change S.map hij (n • S.projection j x) = n • S.projection i x
    induction n with
    | zero =>
        simp only [InverseSystem.projection_apply, zero_nsmul, IsAddGroupSystem.map_zero]
    | succ n ihn =>
        rw [succ_nsmul, succ_nsmul]
        calc
          S.map hij (n • S.projection j x + S.projection j x)
              = S.map hij (n • S.projection j x) + S.map hij (S.projection j x) := by
                  exact IsAddGroupSystem.map_add (S := S) hij (n • S.projection j x)
                    (S.projection j x)
          _ = n • S.projection i x + S.projection i x := by
              rw [ihn, S.projection_compatible x i j hij]⟩
instance

instSMulIntAddInverseLimit

L613 ↗
ProCGroups.InverseSystems.instSMulIntAddInverseLimit
Documentation

An additive inverse limit carries integer scalar multiplication coordinatewise.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · full declaration
instance instSMulIntAddInverseLimit : SMul ℤ S.inverseLimit where
  smul n x := ⟨fun i => n • S.projection i x, by
    intro i j hij
    change S.map hij (n • S.projection j x) = n • S.projection i x
    let f : S.X j →+ S.X i :=
      { toFun := S.map hij
        map_zero' := IsAddGroupSystem.map_zero (S := S) hij
        map_add' := IsAddGroupSystem.map_add (S := S) hij }
    calc
      S.map hij (n • S.projection j x) = f (n • S.projection j x) := rfl
      _ = n • f (S.projection j x) := f.map_zsmul n (S.projection j x)
      _ = n • S.projection i x := by
        change n • S.map hij (S.projection j x) = n • S.projection i x
        rw [S.projection_compatible x i j hij]⟩
theorem

projection_zero

L629 ↗
ProCGroups.InverseSystems.projection_zero
Documentation

The projection of zero is zero at each stage.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · statement
theorem projection_zero (i : I) : S.projection i (0 : S.inverseLimit) = 0
theorem

projection_add

L632 ↗
ProCGroups.InverseSystems.projection_add
Documentation

Projection commutes with addition in an additive inverse system.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · statement
theorem projection_add (i : I) (x y : S.inverseLimit) :
    S.projection i (x + y) = S.projection i x + S.projection i y
theorem

projection_neg

L636 ↗
ProCGroups.InverseSystems.projection_neg
Documentation

Projection commutes with negation in an additive inverse system.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · statement
theorem projection_neg (i : I) (x : S.inverseLimit) :
    S.projection i (-x) = -S.projection i x
theorem

projection_sub

L640 ↗
ProCGroups.InverseSystems.projection_sub
Documentation

Projection commutes with subtraction in an additive inverse system.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · statement
theorem projection_sub (i : I) (x y : S.inverseLimit) :
    S.projection i (x - y) = S.projection i x - S.projection i y
def

instAddCommGroupAddInverseLimit

L647 ↗
ProCGroups.InverseSystems.instAddCommGroupAddInverseLimit
Documentation

The additive-group structure on an additive inverse limit; kept named rather than global to avoid a parent-instance diamond with ring inverse limits.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
Lean source · statement
def instAddCommGroupAddInverseLimit : AddCommGroup S.inverseLimit
instance

instSMulInverseLimitOfIsModuleSystem

L663 ↗
ProCGroups.InverseSystems.instSMulInverseLimitOfIsModuleSystem
Documentation

An inverse-limit module carries scalar multiplication by applying the scalar action at every stage.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
attribute [local instance] instAddCommGroupAddInverseLimit
section ModuleSystems
variable {R : Type w} [Semiring R]
variable [∀ i, Module R (S.X i)] [IsModuleSystem (I := I) R S]
Lean source · full declaration
instance instSMulInverseLimitOfIsModuleSystem : SMul R S.inverseLimit where
  smul r x := ⟨fun i => r • S.projection i x, by
    intro i j hij
    change S.map hij (r • S.projection j x) = r • S.projection i x
    rw [IsModuleSystem.map_smul (S := S) hij, S.projection_compatible x i j hij]⟩
theorem

projection_smul_of_isModuleSystem

L671 ↗
ProCGroups.InverseSystems.projection_smul_of_isModuleSystem
Documentation

Projection commutes with scalar multiplication in a module-valued inverse system.

Source context 16 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
attribute [local instance] instAddCommGroupAddInverseLimit
section ModuleSystems
variable {R : Type w} [Semiring R]
variable [∀ i, Module R (S.X i)] [IsModuleSystem (I := I) R S]
omit [IsAddGroupSystem S] in
Lean source · statement
theorem projection_smul_of_isModuleSystem (i : I) (r : R) (x : S.inverseLimit) :
    S.projection i (r • x) = r • S.projection i x
instance

instModuleInverseLimitOfIsModuleSystem

L676 ↗
ProCGroups.InverseSystems.instModuleInverseLimitOfIsModuleSystem
Documentation

The inverse limit is a module when all stages form a compatible module system.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
attribute [local instance] instAddCommGroupAddInverseLimit
section ModuleSystems
variable {R : Type w} [Semiring R]
variable [∀ i, Module R (S.X i)] [IsModuleSystem (I := I) R S]
Lean source · statement
instance instModuleInverseLimitOfIsModuleSystem : Module R S.inverseLimit
instance

instContinuousSMulInverseLimitOfIsModuleSystem

L684 ↗
ProCGroups.InverseSystems.instContinuousSMulInverseLimitOfIsModuleSystem
Documentation

Scalar multiplication is continuous for the relevant inverse-limit topology.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
attribute [local instance] instAddCommGroupAddInverseLimit
section ModuleSystems
variable {R : Type w} [Semiring R]
variable [∀ i, Module R (S.X i)] [IsModuleSystem (I := I) R S]
Lean source · full declaration
instance instContinuousSMulInverseLimitOfIsModuleSystem
    [TopologicalSpace R] [∀ i, ContinuousSMul R (S.X i)] :
    ContinuousSMul R S.inverseLimit where
  continuous_smul := by
    exact Continuous.subtype_mk
      (continuous_pi fun i =>
        continuous_fst.smul ((S.continuous_projection i).comp continuous_snd))
      (fun p => by
        intro i j hij
        change S.map hij (p.1 • S.projection j p.2) = p.1 • S.projection i p.2
        rw [IsModuleSystem.map_smul (S := S) hij, S.projection_compatible p.2 i j hij])
instance

instIsTopologicalAddGroupAddInverseLimit

L699 ↗
ProCGroups.InverseSystems.instIsTopologicalAddGroupAddInverseLimit
Documentation

The additive inverse-limit object has addition defined coordinatewise on compatible families.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · full declaration
instance instIsTopologicalAddGroupAddInverseLimit [∀ i, IsTopologicalAddGroup (S.X i)] :
    IsTopologicalAddGroup S.inverseLimit where
  continuous_add := by
    exact Continuous.subtype_mk
      (continuous_pi fun i =>
        ((S.continuous_projection i).comp continuous_fst).add
          ((S.continuous_projection i).comp continuous_snd))
      (fun xy => by
        intro i j hij
        change S.map hij (S.projection j xy.1 + S.projection j xy.2) =
          S.projection i xy.1 + S.projection i xy.2
        rw [IsAddGroupSystem.map_add (S := S) hij,
          S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
  continuous_neg := by
    exact Continuous.subtype_mk
      (continuous_pi fun i => continuous_neg.comp (S.continuous_projection i))
      (fun x => by
        intro i j hij
        change S.map hij (-S.projection j x) = -S.projection i x
        rw [IsAddGroupSystem.map_neg (S := S) hij, S.projection_compatible x i j hij])
def

projectionAddHom

L721 ↗
ProCGroups.InverseSystems.projectionAddHom
Documentation

The canonical projections from an additive inverse limit are additive homomorphisms.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · full declaration
def projectionAddHom (i : I) : S.inverseLimit →+ S.X i where
  toFun := S.projection i
  map_zero' := projection_zero (S := S) i
  map_add' := by
    intro x y
    exact projection_add (S := S) i x y
theorem

projectionAddHom_apply

L732 ↗
ProCGroups.InverseSystems.projectionAddHom_apply
Documentation

Applying an additive projection to an inverse-limit element returns its corresponding stage coordinate.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section AddGroupSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
theorem projectionAddHom_apply (i : I) (x : S.inverseLimit) :
    projectionAddHom (S := S) i x = S.projection i x
class

IsRingSystem

L742 ↗
ProCGroups.InverseSystems.IsRingSystem
Documentation

A ring-valued inverse system whose transition maps are ring homomorphisms.

Source context 10 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
Lean source · full declaration
class IsRingSystem (S : InverseSystem (I := I)) [∀ i, Ring (S.X i)] : Prop where
  /-- Transition maps preserve the additive identity. -/
  map_zero : ∀ {i j : I} (hij : i ≤ j), S.map hij 0 = 0
  /-- Transition maps preserve the multiplicative identity. -/
  map_one : ∀ {i j : I} (hij : i ≤ j), S.map hij 1 = 1
  /-- Transition maps preserve addition. -/
  map_add : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
    S.map hij (x + y) = S.map hij x + S.map hij y
  /-- Transition maps preserve multiplication. -/
  map_mul : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
    S.map hij (x * y) = S.map hij x * S.map hij y
def

mapRingHom

L757 ↗
ProCGroups.InverseSystems.mapRingHom
Documentation

A transition map in a ring-valued inverse system is bundled as a ring homomorphism.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
Lean source · full declaration
def mapRingHom {i j : I} (hij : i ≤ j) : S.X j →+* S.X i where
  toFun := S.map hij
  map_zero' := IsRingSystem.map_zero (S := S) hij
  map_one' := IsRingSystem.map_one (S := S) hij
  map_add' := IsRingSystem.map_add (S := S) hij
  map_mul' := IsRingSystem.map_mul (S := S) hij
theorem

mapRingHom_apply

L769 ↗
ProCGroups.InverseSystems.mapRingHom_apply
Documentation

The bundled ring homomorphism has the same underlying function as the coordinatewise construction.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
Lean source · statement
theorem mapRingHom_apply {i j : I} (hij : i ≤ j) (x : S.X j) :
    mapRingHom (S := S) hij x = S.map hij x
theorem

isAddGroupSystemOfIsRingSystem

L774 ↗
ProCGroups.InverseSystems.isAddGroupSystemOfIsRingSystem
Documentation

The additive system underlying a ring system. This remains explicit so that importing ring systems does not install a second global path to the additive inverse-limit instances.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
Lean source · full declaration
theorem isAddGroupSystemOfIsRingSystem : IsAddGroupSystem S where
  map_zero := IsRingSystem.map_zero (S := S)
  map_add := IsRingSystem.map_add (S := S)
  map_neg := by
    intro i j hij x
    exact (mapRingHom (S := S) hij).map_neg x
instance

(anonymous instance)

L781 ↗
Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
Lean source · statement
instance : IsAddGroupSystem S
instance

instMulRingInverseLimit

L789 ↗
ProCGroups.InverseSystems.instMulRingInverseLimit
Documentation

Ring multiplication on the inverse limit is defined coordinatewise through the stage ring multiplications.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · full declaration
instance instMulRingInverseLimit : Mul S.inverseLimit where
  mul x y := ⟨fun i => S.projection i x * S.projection i y, by
    intro i j hij
    calc
      S.map hij (S.projection j x * S.projection j y)
          = S.map hij (S.projection j x) * S.map hij (S.projection j y) := by
              exact IsRingSystem.map_mul (S := S) hij (S.projection j x)
                (S.projection j y)
      _ = S.projection i x * S.projection i y := by
          rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩
instance

instOneRingInverseLimit

L801 ↗
ProCGroups.InverseSystems.instOneRingInverseLimit
Documentation

The unit of the ring inverse limit is the compatible family of units at all stages.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · full declaration
instance instOneRingInverseLimit : One S.inverseLimit where
  one := ⟨fun i => 1, by
    intro i j hij
    exact IsRingSystem.map_one (S := S) hij⟩
instance

instPowNatRingInverseLimit

L807 ↗
ProCGroups.InverseSystems.instPowNatRingInverseLimit
Documentation

Powers in the inverse-limit ring are computed at every stage coordinate.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · full declaration
instance instPowNatRingInverseLimit : Pow S.inverseLimit ℕ where
  pow x n := ⟨fun i => S.projection i x ^ n, by
    intro i j hij
    change S.map hij (S.projection j x ^ n) = S.projection i x ^ n
    rw [← mapRingHom_apply (S := S) hij, map_pow, mapRingHom_apply,
      S.projection_compatible x i j hij]⟩
instance

instNatCastRingInverseLimit

L818 ↗
ProCGroups.InverseSystems.instNatCastRingInverseLimit
Documentation

Natural number casts in a ring inverse limit are computed coordinatewise from finite-stage natural number casts.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · full declaration
instance instNatCastRingInverseLimit : NatCast S.inverseLimit where
  natCast n := ⟨fun _ => n, by
    intro i j hij
    change S.map hij (Nat.cast n) = Nat.cast n
    exact map_natCast (mapRingHom (S := S) hij) n⟩
instance

instIntCastRingInverseLimit

L828 ↗
ProCGroups.InverseSystems.instIntCastRingInverseLimit
Documentation

Integer casts in a ring inverse limit are computed coordinatewise from finite-stage integer casts.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · full declaration
instance instIntCastRingInverseLimit : IntCast S.inverseLimit where
  intCast n := ⟨fun _ => n, by
    intro i j hij
    change S.map hij (Int.cast n) = Int.cast n
    exact map_intCast (mapRingHom (S := S) hij) n⟩
theorem

projection_ring_one

L836 ↗
ProCGroups.InverseSystems.projection_ring_one
Documentation

The inverse-limit projection preserves \(1\).

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
theorem projection_ring_one (i : I) : S.projection i (1 : S.inverseLimit) = 1
theorem

projection_ring_mul

L840 ↗
ProCGroups.InverseSystems.projection_ring_mul
Documentation

The inverse-limit projection preserves multiplication.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
theorem projection_ring_mul (i : I) (x y : S.inverseLimit) :
    S.projection i (x * y) = S.projection i x * S.projection i y
theorem

projection_ring_pow

L845 ↗
ProCGroups.InverseSystems.projection_ring_pow
Documentation

The inverse-limit projection preserves powers.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
theorem projection_ring_pow (i : I) (x : S.inverseLimit) (n : ℕ) :
    S.projection i (x ^ n) = S.projection i x ^ n
theorem

projection_ring_natCast

L850 ↗
ProCGroups.InverseSystems.projection_ring_natCast
Documentation

The inverse-limit projection preserves natural number casts.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
theorem projection_ring_natCast (i : I) (n : ℕ) :
    S.projection i (Nat.cast n : S.inverseLimit) = Nat.cast n
theorem

projection_ring_intCast

L855 ↗
ProCGroups.InverseSystems.projection_ring_intCast
Documentation

The inverse-limit projection preserves integer casts.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
theorem projection_ring_intCast (i : I) (n : ℤ) :
    S.projection i (Int.cast n : S.inverseLimit) = Int.cast n
instance

instRingInverseLimit

L862 ↗
ProCGroups.InverseSystems.instRingInverseLimit
Documentation

A ring inverse limit is a ring because all operations and axioms are inherited coordinatewise from the stage rings.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
instance instRingInverseLimit : Ring S.inverseLimit
instance

instContinuousMulRingInverseLimit

L879 ↗
ProCGroups.InverseSystems.instContinuousMulRingInverseLimit
Documentation

Multiplication in a ring inverse limit is continuous for the inverse-limit topology.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · full declaration
instance instContinuousMulRingInverseLimit [∀ i, ContinuousMul (S.X i)] :
    ContinuousMul S.inverseLimit where
  continuous_mul := by
    exact Continuous.subtype_mk
      (continuous_pi fun i =>
        ((S.continuous_projection i).comp continuous_fst).mul
          ((S.continuous_projection i).comp continuous_snd))
      (fun xy => by
        intro i j hij
        change S.map hij (S.projection j xy.1 * S.projection j xy.2) =
          S.projection i xy.1 * S.projection i xy.2
        rw [IsRingSystem.map_mul (S := S) hij,
          S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
instance

instIsTopologicalRingRingInverseLimit

L897 ↗
ProCGroups.InverseSystems.instIsTopologicalRingRingInverseLimit
Documentation

A ring inverse limit inherits a topological-ring structure from the compatible stage topological rings.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
instance instIsTopologicalRingRingInverseLimit [∀ i, IsTopologicalRing (S.X i)] :
    IsTopologicalRing S.inverseLimit
def

projectionRingHom

L903 ↗
ProCGroups.InverseSystems.projectionRingHom
Documentation

The canonical projection from a ring-valued inverse limit is bundled as a ring homomorphism.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · full declaration
def projectionRingHom (i : I) : S.inverseLimit →+* S.X i where
  toFun := S.projection i
  map_zero' := projection_zero (S := S) i
  map_one' := projection_ring_one (S := S) i
  map_add' := by
    intro x y
    exact projection_add (S := S) i x y
  map_mul' := by
    intro x y
    exact projection_ring_mul (S := S) i x y
theorem

projectionRingHom_apply

L919 ↗
ProCGroups.InverseSystems.projectionRingHom_apply
Documentation

The ring-homomorphism projection has the same underlying coordinate map as the finite-stage projection.

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
theorem projectionRingHom_apply (i : I) (x : S.inverseLimit) :
    projectionRingHom (S := S) i x = S.projection i x
theorem

mapRingHom_comp_projectionRingHom

L926 ↗
ProCGroups.InverseSystems.mapRingHom_comp_projectionRingHom
Documentation

Composing the ring-valued transition from \(j\) to \(i\) with the projection at \(j\) gives the projection at \(i\).

Source context 13 commands

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

open Set
open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v w z
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
section RingSystems
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
variable [∀ i, Ring (S.X i)] [IsRingSystem S]
local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
attribute [local instance] instAddCommGroupAddInverseLimit
Lean source · statement
theorem mapRingHom_comp_projectionRingHom {i j : I} (hij : i ≤ j) :
    (mapRingHom (S := S) hij).comp (projectionRingHom (S := S) j) =
      projectionRingHom (S := S) i

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.