Module

CofinalGroups.lean

Nyll.ProCGroups.InverseSystems.CofinalGroups

3 declarations indexed from sourceView source ↗

Module documentation

Multiplicativity of the existing cofinal restriction

The native homeomorphism already constructs the inverse and proves its continuity. Its forward map is the original coordinate restriction. The existing restricted-system owner supplies both group structures.

Imports3

Imported by2

theorem

directed_subtype_of_cofinal

L28 ↗

ProCGroups.InverseSystems.InverseSystem.directed_subtype_of_cofinal

Documentation

A cofinal subset of a directed preorder is directed.

Source context 4 commands

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

noncomputable section
namespace ProCGroups.InverseSystems.InverseSystem
universe u v
variable {I : Type u} [Preorder I]

Lean source · statement

theorem directed_subtype_of_cofinal
    (T : Set I) (hdir : Directed (· ≤ ·) (id : I → I))
    (hcofinal : ∀ i : I, ∃ t : T, i ≤ t.val) :
    Directed (· ≤ ·) (id : T → T)

def

continuousMulEquiv_restrict_cofinal

L42 ↗

ProCGroups.InverseSystems.InverseSystem.continuousMulEquiv_restrict_cofinal

Documentation

The existing cofinal restriction homeomorphism preserves multiplication.

Source context 5 commands

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

noncomputable section
namespace ProCGroups.InverseSystems.InverseSystem
universe u v
variable {I : Type u} [Preorder I]
variable (S : InverseSystem.{u, v} (I := I))
  [∀ i, Group (S.X i)] [IsGroupSystem S]

Lean source · statement

def continuousMulEquiv_restrict_cofinal
    (T : Set I) (hdir : Directed (· ≤ ·) (id : I → I))
    (hcofinal : ∀ i : I, ∃ t : T, i ≤ t.val) :
    S.inverseLimit ≃ₜ* (S.restrict T).inverseLimit

theorem

projection_continuousMulEquiv_restrict_cofinal

L69 ↗

ProCGroups.InverseSystems.InverseSystem.projection_continuousMulEquiv_restrict_cofinal

Documentation

Restricting a compatible family retains its original coordinate.

Source context 5 commands

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

noncomputable section
namespace ProCGroups.InverseSystems.InverseSystem
universe u v
variable {I : Type u} [Preorder I]
variable (S : InverseSystem.{u, v} (I := I))
  [∀ i, Group (S.X i)] [IsGroupSystem S]

Lean source · statement

theorem projection_continuousMulEquiv_restrict_cofinal
    (T : Set I) (hdir : Directed (· ≤ ·) (id : I → I))
    (hcofinal : ∀ i : I, ∃ t : T, i ≤ t.val)
    (t : T) (x : S.inverseLimit) :
    (S.restrict T).projection t
        ((S.continuousMulEquiv_restrict_cofinal T hdir hcofinal).toFun x) =
      S.projection t.val x

Module documentation

Multiplicativity of the existing cofinal restriction

Declarations

directed_subtype_of_cofinal

continuousMulEquiv_restrict_cofinal

projection_continuousMulEquiv_restrict_cofinal