ProCGroups.NormalSubgroups.SimpleQuotients.Algebraic
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
theorem normal_subgroup_eq_kernel_or_top_of_simple_quotient
{G : Type u} [Group G] (K L : Subgroup G) [K.Normal] (hL : L.Normal)
[IsSimpleGroup (G ⧸ K)] (hKL : K ≤ L) :
L = K ∨ L = ⊤If \(G/K\) is simple, every normal subgroup of \(G\) containing \(K\) is either \(K\) or all of \(G\). This is the correspondence theorem form of the simple-quotient dichotomy.
Show proof
by
haveI : L.Normal := hL
let qL : Subgroup (G ⧸ K) := Subgroup.map (QuotientGroup.mk' K) L
have hqLnormal : qL.Normal := inferInstance
rcases hqLnormal.eq_bot_or_eq_top with hbot | htop
· left
apply le_antisymm
· have hLK : L ≤ K := by
have hker : L ≤ (QuotientGroup.mk' K).ker :=
(Subgroup.map_eq_bot_iff L).mp hbot
simpa [QuotientGroup.ker_mk'] using hker
exact hLK
· exact hKL
· right
have hcomap : Subgroup.comap (QuotientGroup.mk' K) qL = L := by
dsimp [qL]
rw [QuotientGroup.comap_map_mk']
exact sup_of_le_right hKL
rw [← hcomap, htop]
simp only [Subgroup.comap_top]Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem inf_sup_eq_top_of_simple_quotient_dichotomy
{G : Type u} [Group G] (K M N : Subgroup G) [K.Normal] [M.Normal] [N.Normal]
(hsimple : ∀ L : Subgroup G, L.Normal → K ≤ L → L = K ∨ L = ⊤)
(hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
(hMK : M ⊔ K = ⊤) (hNK : N ⊔ K = ⊤) :
M ⊓ N ⊔ K = ⊤Algebraic core of the simple-quotient intersection argument: if subgroups above K satisfy the two-point dichotomy induced by a simple quotient, and the quotient by K is noncommutative, then two normal subgroups whose products with K are all of G have the same property after intersection.
Show proof
by
let L : Subgroup G := M ⊓ N ⊔ K
have hLnormal : L.Normal := inferInstance
have hKleL : K ≤ L := le_sup_right
rcases hsimple L hLnormal hKleL with hLK | hLtop
· exfalso
have hMNK : ⁅M, N⁆ ≤ K := by
exact (Subgroup.commutator_le_inf M N).trans ((le_sup_left : M ⊓ N ≤ L).trans_eq hLK)
have hmapK : Subgroup.map (QuotientGroup.mk' K) K = ⊥ := by
rw [Subgroup.map_eq_bot_iff, QuotientGroup.ker_mk']
have hmapM : Subgroup.map (QuotientGroup.mk' K) M = ⊤ := by
have hmapSup : Subgroup.map (QuotientGroup.mk' K) (M ⊔ K) = ⊤ := by
rw [hMK]
exact Subgroup.map_top_of_surjective (QuotientGroup.mk' K)
(QuotientGroup.mk'_surjective K)
rw [Subgroup.map_sup, hmapK, sup_bot_eq] at hmapSup
exact hmapSup
have hmapN : Subgroup.map (QuotientGroup.mk' K) N = ⊤ := by
have hmapSup : Subgroup.map (QuotientGroup.mk' K) (N ⊔ K) = ⊤ := by
rw [hNK]
exact Subgroup.map_top_of_surjective (QuotientGroup.mk' K)
(QuotientGroup.mk'_surjective K)
rw [Subgroup.map_sup, hmapK, sup_bot_eq] at hmapSup
exact hmapSup
have hcommBot : commutator (G ⧸ K) = ⊥ := by
rw [commutator_def]
nth_rewrite 1 [← hmapM]
nth_rewrite 1 [← hmapN]
rw [← Subgroup.map_commutator]
apply (Subgroup.map_eq_bot_iff ⁅M, N⁆).2
simpa [QuotientGroup.ker_mk'] using hMNK
exact hquotNoncomm hcommBot
· exact hLtopProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem inf_sup_eq_top_of_noncomm_simple_quotient
{G : Type u} [Group G] (K M N : Subgroup G) [K.Normal] [M.Normal] [N.Normal]
[IsSimpleGroup (G ⧸ K)]
(hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
(hMK : M ⊔ K = ⊤) (hNK : N ⊔ K = ⊤) :
M ⊓ N ⊔ K = ⊤Algebraic core with the simple quotient written directly.
Show proof
inf_sup_eq_top_of_simple_quotient_dichotomy K M N
(fun L hL hKL => normal_subgroup_eq_kernel_or_top_of_simple_quotient K L hL hKL)
hquotNoncomm hMK hNKProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□