ProCGroups.InverseSystems.Quotients
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.
def transitionHom {i j : I} (hij : i ≤ j) : S.X j →* S.X i where
toFun := S.map hij
map_one' := IsGroupSystem.map_one (S := S) hij
map_mul' := IsGroupSystem.map_mul (S := S) hijThe transition map of a group-valued inverse system is bundled as a homomorphism.
@[simp] theorem transitionHom_apply {i j : I} (hij : i ≤ j) (x : S.X j) :
S.transitionHom hij x = S.map hij xThe quotient inverse-system transition homomorphism sends a quotient class to its image under the transition map.
Show proof
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 continuous_transitionHom {i j : I} (hij : i ≤ j) :
Continuous (S.transitionHom hij)The bundled transition homomorphism of an inverse system is continuous.
Show proof
S.continuous_map hijProof. 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.
□structure CompatibleClosedNormalSubgroups where
N : ∀ i, Subgroup (S.X i)
normal : ∀ i, (N i).Normal
closed : ∀ i, IsClosed ((N i : Subgroup (S.X i)) : Set (S.X i))
map_le :
∀ {i j : I} (hij : i ≤ j), N j ≤ (N i).comap (S.transitionHom hij)Closed normal subgroups of the stages, compatible with transition maps.
instance instNormalN (i : I) : (Q.N i).Normal := Q.normal iThe chosen subgroup is normal.
def quotientMap {i j : I} (hij : i ≤ j) :
S.X j ⧸ Q.N j →* S.X i ⧸ Q.N i :=
QuotientGroup.map (N := Q.N j) (M := Q.N i) (f := S.transitionHom hij) (Q.map_le hij)The transition map induced on stage quotients.
@[simp] theorem quotientMap_mk {i j : I} (hij : i ≤ j) (x : S.X j) :
Q.quotientMap hij (QuotientGroup.mk' (Q.N j) x) =
QuotientGroup.mk' (Q.N i) (S.map hij x)The compatible closed normal subgroup family induces the expected quotient inverse-system map.
Show proof
by
exact QuotientGroup.map_mk' (N := Q.N j) (M := Q.N i)
(f := S.transitionHom hij) (Q.map_le hij) xProof. 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 continuous_quotientMap {i j : I} (hij : i ≤ j) :
Continuous (Q.quotientMap hij)The induced map on stage quotients is continuous.
Show proof
by
refine (QuotientGroup.isQuotientMap_mk (N := Q.N j)).continuous_iff.2 ?_
change Continuous fun x : S.X j => QuotientGroup.mk' (Q.N i) (S.map hij x)
exact QuotientGroup.continuous_mk.comp (S.continuous_map hij)Proof. 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.
□def quotientInverseSystem : InverseSystem (I := I) where
X := fun i => S.X i ⧸ Q.N i
topologicalSpace := fun i => inferInstance
map := fun {_i _j} hij => Q.quotientMap hij
continuous_map := fun {_i _j} hij => Q.continuous_quotientMap hij
map_id := by
intro i
funext x
refine Quotient.inductionOn' x ?_
intro a
change QuotientGroup.mk' (Q.N i) (S.map (le_rfl : i ≤ i) a) =
QuotientGroup.mk' (Q.N i) a
exact congrArg (QuotientGroup.mk' (Q.N i)) (S.map_id_apply i a)
map_comp := by
intro i j k hij hjk
funext x
refine Quotient.inductionOn' x ?_
intro a
change QuotientGroup.mk' (Q.N i) (S.map hij (S.map hjk a)) =
QuotientGroup.mk' (Q.N i) (S.map (hij.trans hjk) a)
exact congrArg (QuotientGroup.mk' (Q.N i)) (S.map_comp_apply hij hjk a)The inverse system obtained by quotienting each stage by a compatible closed normal subgroup.
instance quotientInverseSystem_stageGroup (i : I) :
Group (Q.quotientInverseSystem.X i) := by
change Group (S.X i ⧸ Q.N i)
infer_instanceThe quotient inverse system has the expected finite-stage quotient groups.
instance quotientInverseSystem_stageTopologicalGroup (i : I) :
IsTopologicalGroup (Q.quotientInverseSystem.X i) := by
change IsTopologicalGroup (S.X i ⧸ Q.N i)
infer_instanceThe compatible closed normal subgroup family induces the expected quotient inverse-system map.
instance quotientInverseSystem_isGroupSystem :
IsGroupSystem Q.quotientInverseSystem where
map_one := by
intro i j hij
exact (Q.quotientMap hij).map_one
map_mul := by
intro i j hij x y
exact (Q.quotientMap hij).map_mul x y
map_inv := by
intro i j hij x
exact (Q.quotientMap hij).map_inv xThe finite-stage inverse system carries the bundled structure determined by its transition maps.
def toQuotientInverseSystem : S.Morphism Q.quotientInverseSystem where
map := fun i => QuotientGroup.mk' (Q.N i)
continuous_map := fun _ => QuotientGroup.continuous_mk
comm := by
intro i j hij
funext x
exact (Q.quotientMap_mk hij x).symmThe stagewise quotient maps form a morphism from the original system to the quotient system.
def inverseLimitKernel : Subgroup S.inverseLimit :=
⨅ i, (Q.N i).comap (projectionHom (S := S) i)Kernel of the map from the inverse limit to the inverse limit of stage quotients.
instance inverseLimitKernel_normal : Q.inverseLimitKernel.Normal where
conj_mem x hx g := by
rw [inverseLimitKernel] at hx ⊢
simp only [projectionHom, Subgroup.mem_iInf, Subgroup.mem_comap, MonoidHom.coe_mk, OneHom.coe_mk,
projection_apply] at hx ⊢
intro i
simpa using (Q.normal i).conj_mem (S.projection i x) (hx i) (S.projection i g)The compatible closed normal subgroup family induces the expected quotient inverse-system map.
theorem mem_inverseLimitKernel_iff (x : S.inverseLimit) :
x ∈ Q.inverseLimitKernel ↔ ∀ i, S.projection i x ∈ Q.N iMembership in the named kernel is equivalent to vanishing under its defining quotient or augmentation map.
Show proof
by
simp only [inverseLimitKernel, projectionHom, Subgroup.mem_iInf, Subgroup.mem_comap, MonoidHom.coe_mk,
OneHom.coe_mk, projection_apply]Proof. 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.
□noncomputable def quotientInverseLimitComparison :
S.inverseLimit ⧸ Q.inverseLimitKernel →ₜ* Q.quotientInverseSystem.inverseLimit := by
let T : InverseSystem (I := I) := Q.quotientInverseSystem
let φ : S.inverseLimit →ₜ* T.inverseLimit :=
{ toMonoidHom :=
{ toFun := S.limMap Q.toQuotientInverseSystem
map_one' := by
apply T.ext
intro i
calc
T.projection i (S.limMap Q.toQuotientInverseSystem 1) =
Q.toQuotientInverseSystem.map i (S.projection i (1 : S.inverseLimit)) := by
exact S.π_limMap_apply Q.toQuotientInverseSystem i 1
_ = 1 := by
change QuotientGroup.mk' (Q.N i) (S.projection i (1 : S.inverseLimit)) = 1
rw [projection_one (S := S) i]
simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one]
map_mul' := by
intro x y
apply T.ext
intro i
calc
T.projection i (S.limMap Q.toQuotientInverseSystem (x * y)) =
Q.toQuotientInverseSystem.map i (S.projection i (x * y)) := by
exact S.π_limMap_apply Q.toQuotientInverseSystem i (x * y)
_ =
Q.toQuotientInverseSystem.map i (S.projection i x) *
Q.toQuotientInverseSystem.map i (S.projection i y) := by
change QuotientGroup.mk' (Q.N i) (S.projection i (x * y)) =
QuotientGroup.mk' (Q.N i) (S.projection i x) *
QuotientGroup.mk' (Q.N i) (S.projection i y)
rw [projection_mul (S := S) i x y]
simp only [projection_apply, QuotientGroup.mk'_apply, QuotientGroup.mk_mul]
_ =
T.projection i (S.limMap Q.toQuotientInverseSystem x) *
T.projection i (S.limMap Q.toQuotientInverseSystem y) := by
rw [← S.π_limMap_apply Q.toQuotientInverseSystem i x,
← S.π_limMap_apply Q.toQuotientInverseSystem i y] }
continuous_toFun := S.continuous_limMap Q.toQuotientInverseSystem }
refine QuotientGroup.liftₜ Q.inverseLimitKernel φ ?_
intro x hx
apply T.ext
intro i
have hxi : S.projection i x ∈ Q.N i := (Q.mem_inverseLimitKernel_iff x).1 hx i
change QuotientGroup.mk' (Q.N i) (S.projection i x) = 1
exact (QuotientGroup.eq_one_iff (N := Q.N i) (S.projection i x)).2 hxiThe canonical comparison from the quotient of the inverse limit to the inverse limit of the stage quotients.
@[simp] theorem quotientInverseLimitComparison_mk (x : S.inverseLimit) :
Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x) =
S.limMap Q.toQuotientInverseSystem xThe quotient inverse-limit comparison sends a representative to its compatible family of quotient coordinates.
Show proof
by
unfold quotientInverseLimitComparison
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.
□@[simp] theorem projection_quotientInverseLimitComparison_mk
(i : I) (x : S.inverseLimit) :
Q.quotientInverseSystem.projection i
(Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x)) =
QuotientGroup.mk' (Q.N i) (S.projection i x)Projecting the quotient inverse-limit comparison gives the corresponding stage quotient representative.
Show proof
by
rw [quotientInverseLimitComparison_mk]
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 ker_quotientInverseLimitComparison :
Q.quotientInverseLimitComparison.toMonoidHom.ker = ⊥The comparison map has trivial kernel.
Show proof
by
ext a
constructor
· intro ha
refine Quotient.inductionOn' a ?_ ha
intro x hx
rw [MonoidHom.mem_ker] at hx
rw [Subgroup.mem_bot]
exact (QuotientGroup.eq_one_iff (N := Q.inverseLimitKernel) x).2 <| by
rw [Q.mem_inverseLimitKernel_iff]
intro i
have hcoord :=
congrArg (fun y => Q.quotientInverseSystem.projection i y) hx
change QuotientGroup.mk' (Q.N i) (S.projection i x) = 1 at hcoord
exact (QuotientGroup.eq_one_iff (N := Q.N i) (S.projection i x)).1 hcoord
· intro ha
rw [Subgroup.mem_bot] at ha
rw [MonoidHom.mem_ker, ha]
exact map_one Q.quotientInverseLimitComparisonProof. 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 injective_quotientInverseLimitComparison :
Function.Injective Q.quotientInverseLimitComparisonThe comparison map is injective: its kernel is exactly the subgroup used in the quotient.
Show proof
(MonoidHom.ker_eq_bot_iff (f := Q.quotientInverseLimitComparison.toMonoidHom)).mp
Q.ker_quotientInverseLimitComparisonProof. 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 surjective_quotientInverseLimitComparison
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I)) :
Function.Surjective Q.quotientInverseLimitComparisonThe comparison map is surjective for compact Hausdorff systems over a directed index.
Show proof
by
let T : InverseSystem (I := I) := Q.quotientInverseSystem
letI : ∀ i, T2Space (T.X i) := fun i => by
dsimp [T, quotientInverseSystem]
haveI : IsClosed ((Q.N i : Subgroup (S.X i)) : Set (S.X i)) := Q.closed i
infer_instance
have hlimsurj : Function.Surjective (S.limMap Q.toQuotientInverseSystem) :=
S.surjective_limMap (T := T) hdir Q.toQuotientInverseSystem
(fun i => QuotientGroup.mk'_surjective (Q.N i))
intro y
rcases hlimsurj y with ⟨x, hx⟩
refine ⟨QuotientGroup.mk' Q.inverseLimitKernel x, ?_⟩
simpa [quotientInverseLimitComparison_mk] using hxProof. 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 bijective_quotientInverseLimitComparison
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I)) :
Function.Bijective Q.quotientInverseLimitComparisonThe comparison map is bijective for compact Hausdorff systems over a directed index.
Show proof
⟨Q.injective_quotientInverseLimitComparison,
Q.surjective_quotientInverseLimitComparison hdir⟩Proof. 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.
□noncomputable def quotientInverseLimitContinuousMulEquiv
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I)) :
S.inverseLimit ⧸ Q.inverseLimitKernel ≃ₜ* Q.quotientInverseSystem.inverseLimit := by
let T : InverseSystem (I := I) := Q.quotientInverseSystem
let f := Q.quotientInverseLimitComparison
letI : CompactSpace S.inverseLimit := inferInstance
letI : CompactSpace (S.inverseLimit ⧸ Q.inverseLimitKernel) := inferInstance
letI : ∀ i, T2Space (T.X i) := fun i => by
dsimp [T, quotientInverseSystem]
haveI : IsClosed ((Q.N i : Subgroup (S.X i)) : Set (S.X i)) := Q.closed i
infer_instance
letI : T2Space T.inverseLimit := T.t2Space_inverseLimit
exact ContinuousMulEquiv.ofBijectiveCompactToT2
f.toMonoidHom f.continuous_toFun (Q.bijective_quotientInverseLimitComparison hdir)The quotient of an inverse limit by a compatible closed normal family is the inverse limit of the stage quotients.