EtaleFundamentalGroups.Inertia.primeToRootsSystem_restrict_isGroupSystem
The literal restricted root system is a group system for the SAME prime-to-roots groups, with the full exponent family closed in this owner.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u vLean source · full declaration
theorem primeToRootsSystem_restrict_isGroupSystem
(k : Type u) (R : Type v) [Field k] [Field R]
(J : Set (InvertibleExponent k)) :
let : ∀ j : J, Group (((primeToRootsSystem k R).restrict J).X j) :=
fun j => primeToRootsSystem_group k R j.val
IsGroupSystem ((primeToRootsSystem k R).restrict J) := by
intro rootGroups
let fullGroups : ∀ n : InvertibleExponent k, Group ((primeToRootsSystem k R).X n) :=
fun n => primeToRootsSystem_group k R n
have fullGroupSystem : IsGroupSystem (primeToRootsSystem k R) :=
primeToRootsSystem_isGroupSystem k R
exact InverseSystem.restrict_isGroupSystem (primeToRootsSystem k R) J