ProCGroups.InverseSystems.ProfiniteLimits
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
Imported by
def inverseLimitProjectionHom {I : Type v} [Preorder I]
(S : InverseSystems.InverseSystem (I := I))
[∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S] (i : I) :
S.inverseLimit →* S.X i where
toFun := S.projection i
map_one' := rfl
map_mul' := by
intro x y
rflThe projection from a group-valued inverse limit to one component is viewed as a homomorphism.
def inverseLimitProjectionKer {I : Type v} [Preorder I]
(S : InverseSystems.InverseSystem (I := I))
[∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
[∀ i, DiscreteTopology (S.X i)] (i : I) :
OpenNormalSubgroup S.inverseLimit where
toOpenSubgroup :=
{ toSubgroup := (inverseLimitProjectionHom S i).ker
isOpen' := by
change IsOpen {x : S.inverseLimit | inverseLimitProjectionHom S i x = 1}
simpa [inverseLimitProjectionHom] using
(isOpen_discrete ({1} : Set (S.X i))).preimage (S.continuous_projection i) }
isNormal' := by
change ((inverseLimitProjectionHom S i).ker).Normal
infer_instanceThe kernel of a projection from an inverse limit of discrete groups is open normal.
@[simp] theorem mem_inverseLimitProjectionKer {I : Type v} [Preorder I]
{S : InverseSystems.InverseSystem (I := I)}
[∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
[∀ i, DiscreteTopology (S.X i)]
{i : I} {x : S.inverseLimit} :
x ∈ inverseLimitProjectionKer S i ↔ S.projection i x = 1Membership in the kernel of an inverse-limit projection is membership in the kernel at that finite stage.
Show proof
Iff.rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem exists_inverseLimitProjectionKer_sub_open_nhds_of_one
{I : Type v} [Preorder I]
(S : InverseSystems.InverseSystem (I := I)) [Nonempty I]
[∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
[∀ i, DiscreteTopology (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
{W : Set S.inverseLimit} (hW : IsOpen W) (h1W : (1 : S.inverseLimit) ∈ W) :
∃ i : I,
(((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
Subgroup S.inverseLimit) : Set S.inverseLimit) ⊆ WIn an inverse limit of discrete groups, every open neighborhood of \(1\) contains the kernel of one projection map.
Show proof
by
rcases S.exists_projection_preimage_subset hdir hW h1W with ⟨i, V, -, h1V, hVW⟩
refine ⟨i, ?_⟩
intro x hx
have hxker : S.projection i x = 1 := (mem_inverseLimitProjectionKer (S := S) (i := i)).1 hx
have hV1 : (1 : S.X i) ∈ V := h1V
have hxV : x ∈ S.projection i ⁻¹' V := by
change S.projection i x ∈ V
rw [hxker]
exact hV1
exact hVW hxVProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem inverseLimitProjectionKer_fundamentalSystemAtOne
{I : Type v} [Preorder I]
(S : InverseSystems.InverseSystem (I := I)) [Nonempty I]
[∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
[∀ i, DiscreteTopology (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I)) :
(∀ i : I,
IsOpen ((((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
Subgroup S.inverseLimit) : Set S.inverseLimit)) ∧
(1 : S.inverseLimit) ∈ (((inverseLimitProjectionKer S i :
OpenNormalSubgroup S.inverseLimit) : Subgroup S.inverseLimit) : Set S.inverseLimit)) ∧
∀ W : Set S.inverseLimit, IsOpen W → (1 : S.inverseLimit) ∈ W →
∃ i : I,
((((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
Subgroup S.inverseLimit) : Set S.inverseLimit)) ⊆ WThe projection kernels form a fundamental system of open neighborhoods of 1 in the inverse limit.
Show proof
by
refine ⟨?_, ?_⟩
· intro i
refine ⟨openNormalSubgroup_isOpen (G := S.inverseLimit) (inverseLimitProjectionKer S i), ?_⟩
change ((1 : S.inverseLimit).1 i) = 1
rfl
· intro W hW h1W
exact exists_inverseLimitProjectionKer_sub_open_nhds_of_one S hdir hW h1WProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□