NYLL
Module

GroupSystemRestriction.lean

Nyll.ProCGroups.InverseSystems.GroupSystemRestriction
2 declarations indexed from sourceView source ↗

Module documentation

Group structures on restricted inverse systems

The existing restriction keeps the stage groups and transition homomorphisms. This canonical instance permits both homomorphisms to the restricted limit and its coordinatewise group laws to use the original inverse-system owner.

Imports1
Imported by3

Declarations

instance

restrict_groups

L24 ↗
ProCGroups.InverseSystems.InverseSystem.restrict_groups
Source context 3 commands

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

namespace ProCGroups.InverseSystems
universe u v
variable {I : Type u} [Preorder I] (S : InverseSystem.{u, v} (I := I))
  [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · statement
instance InverseSystem.restrict_groups (J : Set I) :
    ∀ j : J, Group ((S.restrict J).X j)
instance

restrict_isGroupSystem

L28 ↗
ProCGroups.InverseSystems.InverseSystem.restrict_isGroupSystem
Source context 3 commands

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

namespace ProCGroups.InverseSystems
universe u v
variable {I : Type u} [Preorder I] (S : InverseSystem.{u, v} (I := I))
  [∀ i, Group (S.X i)] [IsGroupSystem S]
Lean source · full declaration
instance InverseSystem.restrict_isGroupSystem (J : Set I) :
    IsGroupSystem (S.restrict J) where
  map_one := fun {_ _} h => IsGroupSystem.map_one (S := S) h
  map_mul := fun {_ _} h x y => IsGroupSystem.map_mul (S := S) h x y
  map_inv := fun {_ _} h x => IsGroupSystem.map_inv (S := S) h x

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