Grace/Cumulus/Algebra/Group/Quotient.g17

Open in Workbench Download source

Imports

Normal · Relation.QuotientOperations

Declarations

Source

1-- Quotient groups: the coset relation of a subgroup is an equivalence2-- whose classes are the left cosets, a normal subgroup makes it a3-- congruence, the quotient carries the induced group structure, and the4-- projection is a surjective homomorphism with the normal subgroup as its5-- kernel6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Group.Quotient12import Normal13import Relation.QuotientOperations1415-- x and y are related when x⁻¹ * y lies in N.16def cosetRelation (G N : Set) : Set :=17  { p ∈ G.carrier × G.carrier | ∃ x ∈ G.carrier, ∃ y ∈ G.carrier,18    p = (x, y) ∧ G.mul(G.inv(x), y) ∈ N }1920-- The quotient group of G by N: the classes of the coset relation with the21-- induced operation, unit, and inverse.22def quotientGroup (G N : Set) : Set :=23  Group.mk((G.carrier ⧸ cosetRelation(G, N)),24    quotientBinary(G.carrier, cosetRelation(G, N), G.mul),25    ⟦G.one⟧[G.carrier, cosetRelation(G, N)],26    quotientUnary(G.carrier, cosetRelation(G, N), G.inv))2728-- The quotient is written G ⧸ N wherever G is the group of a hypothesis in29-- scope; the set quotient A ⧸ r keeps its meaning on every other left30-- operand.31notation infixl 70 "⧸" => quotientGroup(G, _) via hypothesis Group(G) for G32notation infixl 70 "⧸" => quotientGroup(G, _) via hypothesis NormalSubgroup(N, G) for G3334theorem quotientGroup.carrierOf (G N : Set)35  shows Group.carrier(quotientGroup(G, N)) = (G.carrier ⧸ cosetRelation(G, N))36proof37  simp [quotientGroup, Group.mk.carrier]3839theorem quotientGroup.operation (G N : Set)40  shows Group.mul(quotientGroup(G, N)) = quotientBinary(G.carrier, cosetRelation(G, N), G.mul)41proof42  simp [quotientGroup, Group.mk.mul]4344theorem quotientGroup.unit (G N : Set)45  shows Group.one(quotientGroup(G, N)) = ⟦G.one⟧[G.carrier, cosetRelation(G, N)]46proof47  simp [quotientGroup, Group.mk.one]4849theorem quotientGroup.inverse (G N : Set)50  shows Group.inv(quotientGroup(G, N)) = quotientUnary(G.carrier, cosetRelation(G, N), G.inv)51proof52  simp [quotientGroup, Group.mk.inv]5354theorem cosetRelation.relation (G N : Set)55  shows RelationOn(cosetRelation(G, N), G.carrier)56proof57  intros p hp58  have parts := cosetRelation.membership.forward with hp59  exact parts.left6061section CosetRelation62variable (G N : Set)63hypothesis group : Group(G)64hypothesis subgroup : Subgroup(N, G)6566theorem cosetRelation.relates (x y : G)67  shows relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N68proof69  constructor70  . intro related71    obtain ⟨bounded, u, hu, v, hv, shape, member⟩ :=72      cosetRelation.membership.forward at G, N, (x, y) with related73    have coordinates := orderedPair.injective with shape74    rwa [coordinates.left, coordinates.right]75  . intro member76    have xIn : x ∈ G by assumption77    have yIn : y ∈ G by assumption78    have bounded := product.pair at x, y, G.carrier, G.carrier with *79    unfold relates80    apply cosetRelation.membership.backward81    refine ⟨bounded, x, xIn, y, yIn, rfl, member⟩8283theorem cosetRelation.equivalence84  shows Equivalence(G.carrier, cosetRelation(G, N))85proof86  have relation := cosetRelation.relation at G, N87  unfold Equivalence88  refine ⟨relation, ?_, ?_, ?_⟩89  . intros x hx90    have criterion : relates(cosetRelation(G, N), x, x) ↔ x⁻¹ * x ∈ N := cosetRelation.relates with *91    apply criterion.backward92    rw Group.inv_mul93    exact Subgroup.one_mem with *94  . intros x hx y hy related95    have forward : relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N := cosetRelation.relates with *96    have backward : relates(cosetRelation(G, N), y, x) ↔ y⁻¹ * x ∈ N := cosetRelation.relates with *97    have member := forward.forward with related98    have inverted : (x⁻¹ * y)⁻¹ ∈ N := Subgroup.inv_mem with *99    rw [mul_inv_rev, inv_inv] at inverted100    exact backward.backward with inverted101  . intros x hx y hy z hz xy yz102    have first : relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N := cosetRelation.relates with *103    have second : relates(cosetRelation(G, N), y, z) ↔ y⁻¹ * z ∈ N := cosetRelation.relates with *104    have third : relates(cosetRelation(G, N), x, z) ↔ x⁻¹ * z ∈ N := cosetRelation.relates with *105    have firstIn := first.forward with xy106    have secondIn := second.forward with yz107    have product : x⁻¹ * y * (y⁻¹ * z) ∈ N := Subgroup.mul_mem with *108    rw [mul_assoc, mul_inv_cancel_left] at product109    exact third.backward with product110111-- The equivalence classes are the left cosets.112theorem cosetRelation.class_eq_coset (x : G)113  shows ⟦x⟧[G.carrier, cosetRelation(G, N)] = leftCoset(G, x, N)114proof115  ext y116  constructor117  . intro hy118    obtain ⟨yIn, related⟩ := equivalenceClass.membership.forward with hy119    have criterion : relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N := cosetRelation.relates with *120    have cosetCriterion : y ∈ leftCoset(G, x, N) ↔ x⁻¹ * y ∈ N := leftCoset.mem_iff with *121    have member := criterion.forward with related122    exact cosetCriterion.backward with member123  . intro hy124    have yIn := leftCoset.subset at G, x, N with y, hy125    have criterion : relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N := cosetRelation.relates with *126    have cosetCriterion : y ∈ leftCoset(G, x, N) ↔ x⁻¹ * y ∈ N := leftCoset.mem_iff with *127    have member := cosetCriterion.forward with hy128    have related := criterion.backward with member129    exact equivalenceClass.membership.backward with ⟨yIn, related⟩130131theorem cosetRelation.quotient_eq_cosets132  shows (G.carrier ⧸ cosetRelation(G, N)) = leftCosets(G, N)133proof134  have equivalence := cosetRelation.equivalence with group, subgroup135  ext C136  constructor137  . intro hC138    obtain ⟨bounded, x, hx, shape⟩ := quotient.membership.forward with hC139    have coset : ⟦x⟧[G.carrier, cosetRelation(G, N)] = leftCoset(G, x, N) := cosetRelation.class_eq_coset with *140    rw [shape, coset]141    exact leftCosets.coset_member with hx142  . intro hC143    obtain ⟨bounded, x, hx, shape⟩ := leftCosets.membership.forward with hC144    have coset : ⟦x⟧[G.carrier, cosetRelation(G, N)] = leftCoset(G, x, N) := cosetRelation.class_eq_coset with *145    rw [shape, ← coset]146    exact quotient.contains_class with equivalence, hx147148theorem cosetRelation.class_eq_iff (x y : G)149  shows ⟦x⟧[G.carrier, cosetRelation(G, N)] = ⟦y⟧[G.carrier, cosetRelation(G, N)] ↔ x⁻¹ * y ∈ N150proof151  have equivalence := cosetRelation.equivalence with group, subgroup152  have criterion : relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N := cosetRelation.relates with *153  constructor154  . intro equal155    have related := equivalenceClass.related_of_eq with equivalence, *156    exact criterion.forward with related157  . intro member158    have related := criterion.backward with member159    exact equivalenceClass.eq with equivalence, *160161theorem cosetRelation.class_eq_one_iff (x : G)162  shows ⟦x⟧[G.carrier, cosetRelation(G, N)] = ⟦G.one⟧[G.carrier, cosetRelation(G, N)] ↔ x ∈ N163proof164  have criterion : ⟦x⟧[G.carrier, cosetRelation(G, N)] = ⟦G.one⟧[G.carrier, cosetRelation(G, N)] ↔165      x⁻¹ * G.one ∈ N := cosetRelation.class_eq_iff with *166  have inverseCriterion : x⁻¹ ∈ N ↔ x ∈ N := Subgroup.inv_mem_iff with *167  rw mul_one at criterion168  constructor169  . intro equal170    have member := criterion.forward with equal171    exact inverseCriterion.forward with member172  . intro member173    have inverted := inverseCriterion.backward with member174    exact criterion.backward with inverted175176instance quotientGroup.class_mem (x : G)177  shows ⟦x⟧[G.carrier, cosetRelation(G, N)] ∈ Group.carrier(G ⧸ N)178proof179  have equivalence := cosetRelation.equivalence with group, subgroup180  rw quotientGroup.carrierOf181  exact quotient.contains_class with equivalence, *182183theorem quotientGroup.representative (X : Set)184  requires hX : X ∈ Group.carrier(G ⧸ N)185  shows ∃ x ∈ G, X = ⟦x⟧[G.carrier, cosetRelation(G, N)]186proof187  rw quotientGroup.carrierOf at hX188  exact quotient.representative with hX189190end CosetRelation191192section QuotientGroup193variable (G N : Set)194hypothesis group : Group(G)195hypothesis normal : NormalSubgroup(N, G)196197-- Normality makes the coset relation a congruence.198theorem cosetRelation.mul_compatible199  shows CompatibleBinary(G.carrier, cosetRelation(G, N), G.mul)200proof201  have subgroup := NormalSubgroup.subgroup with normal202  intros x hx y hy u hu v hv xy uv203  have first : relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N := cosetRelation.relates with *204  have second : relates(cosetRelation(G, N), u, v) ↔ u⁻¹ * v ∈ N := cosetRelation.relates with *205  have target : relates(cosetRelation(G, N), x * u, y * v) ↔ (x * u)⁻¹ * (y * v) ∈ N :=206    cosetRelation.relates with *207  have firstIn := first.forward with xy208  have secondIn := second.forward with uv209  have conj : u⁻¹ * (x⁻¹ * y) * u ∈ N := NormalSubgroup.inv_mul_mem with *210  have product : u⁻¹ * (x⁻¹ * y) * u * (u⁻¹ * v) ∈ N := Subgroup.mul_mem with *211  have same : (x * u)⁻¹ * (y * v) = u⁻¹ * (x⁻¹ * y) * u * (u⁻¹ * v)212    rw mul_inv_rev213    group_simp214  rw ← same at product215  exact target.backward with product216217theorem cosetRelation.inv_compatible218  shows CompatibleUnary(G.carrier, cosetRelation(G, N), G.inv)219proof220  have subgroup := NormalSubgroup.subgroup with normal221  intros x hx y hy xy222  have criterion : relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N := cosetRelation.relates with *223  have target : relates(cosetRelation(G, N), x⁻¹, y⁻¹) ↔ (x⁻¹)⁻¹ * y⁻¹ ∈ N := cosetRelation.relates with *224  have member := criterion.forward with xy225  have inverted : (x⁻¹ * y)⁻¹ ∈ N := Subgroup.inv_mem with *226  have conj : x * (x⁻¹ * y)⁻¹ * x⁻¹ ∈ N := NormalSubgroup.mul_mem with *227  have same : (x⁻¹)⁻¹ * y⁻¹ = x * (x⁻¹ * y)⁻¹ * x⁻¹228    rw [inv_inv, mul_inv_rev, inv_inv]229    group_simp230  rw ← same at conj231  exact target.backward with conj232233-- The quotient group.234theorem quotientGroup.group235  shows Group(G ⧸ N)236proof237  have subgroup := NormalSubgroup.subgroup with normal238  have equivalence := cosetRelation.equivalence with group, subgroup239  have compatible := cosetRelation.mul_compatible with group, normal240  have invCompatible := cosetRelation.inv_compatible with group, normal241  have parts := Group.parts with group242  have magma := IsGroup.magma with parts243  have monoid := IsGroup.monoid with parts244  have associative := IsMonoid.associative with monoid245  have identity := IsMonoid.identity with monoid246  have inverseLaw := IsGroup.inverse with parts247  have qMagma := quotientBinary.magma with equivalence, magma, compatible248  have qAssociative := quotientBinary.associative with equivalence, magma, compatible, associative249  have qIdentity := quotientBinary.identity with equivalence, magma, compatible, identity250  have qInverse := quotientUnary.inverse with equivalence, magma, compatible, invCompatible, inverseLaw251  unfold quotientGroup252  apply Group.of_parts253  simp [IsGroup, IsMonoid, IsSemigroup]254255theorem quotientGroup.mul_class (x y : G)256  shows Group.mul(G ⧸ N)(⟦x⟧[G.carrier, cosetRelation(G, N)], ⟦y⟧[G.carrier, cosetRelation(G, N)]) =257    ⟦x * y⟧[G.carrier, cosetRelation(G, N)]258proof259  have subgroup := NormalSubgroup.subgroup with normal260  have equivalence := cosetRelation.equivalence with group, subgroup261  have compatible := cosetRelation.mul_compatible with group, normal262  have magma := IsGroup.magma with (Group.parts with group)263  rw quotientGroup.operation264  exact quotientBinary.classes with equivalence, magma, compatible, *265266theorem quotientGroup.inv_class (x : G)267  shows Group.inv(G ⧸ N)(⟦x⟧[G.carrier, cosetRelation(G, N)]) =268    ⟦x⁻¹⟧[G.carrier, cosetRelation(G, N)]269proof270  have subgroup := NormalSubgroup.subgroup with normal271  have equivalence := cosetRelation.equivalence with group, subgroup272  have invCompatible := cosetRelation.inv_compatible with group, normal273  have function := Group.inverse_function with group274  rw quotientGroup.inverse275  exact quotientUnary.classes with equivalence, function, invCompatible, *276277theorem quotientGroup.abelian278  requires abelian : AbelianGroup(G)279  shows AbelianGroup(G ⧸ N)280proof281  have commutative := IsAbelianGroup.commutative with (AbelianGroup.parts with abelian)282  have subgroup := NormalSubgroup.subgroup with normal283  have equivalence := cosetRelation.equivalence with group, subgroup284  have compatible := cosetRelation.mul_compatible with group, normal285  have magma := IsGroup.magma with (Group.parts with group)286  have qgroup := quotientGroup.group with group, normal287  have qParts := Group.parts with qgroup288  have qCommutative := quotientBinary.commutative with equivalence, magma, compatible, commutative289  rw [quotientGroup.carrierOf, quotientGroup.operation, quotientGroup.unit, quotientGroup.inverse] at qParts290  unfold quotientGroup291  apply AbelianGroup.of_parts292  unfold IsAbelianGroup293  exact ⟨qParts, qCommutative⟩294295-- The projection onto the quotient.296theorem quotientGroup.projection_hom297  shows quotientProjection(G.carrier, cosetRelation(G, N)) : G →* G ⧸ N298proof299  have subgroup := NormalSubgroup.subgroup with normal300  have equivalence := cosetRelation.equivalence with group, subgroup301  have qgroup := quotientGroup.group with group, normal302  have function := quotientProjection.function at G.carrier, cosetRelation(G, N) with equivalence303  have projection : quotientProjection(G.carrier, cosetRelation(G, N)) : G.carrier → Group.carrier(G ⧸ N)304    rw quotientGroup.carrierOf305    exact function306  apply GroupHom.mk with group, qgroup, projection307  intros x hx y hy308  have closed : x * y ∈ G by typecheck309  have vx := quotientProjection.value at G.carrier, cosetRelation(G, N), x with *310  have vy := quotientProjection.value at G.carrier, cosetRelation(G, N), y with *311  have output := quotientProjection.value at G.carrier, cosetRelation(G, N), x * y with *312  have lifted := quotientGroup.mul_class with group, normal, hx, hy313  cc314315theorem quotientGroup.projection_surjective316  shows SurjectiveBetween(quotientProjection(G.carrier, cosetRelation(G, N)), G.carrier,317    Group.carrier(G ⧸ N))318proof319  have subgroup := NormalSubgroup.subgroup with normal320  have equivalence := cosetRelation.equivalence with group, subgroup321  rw quotientGroup.carrierOf322  exact quotientProjection.surjective with equivalence323324theorem quotientGroup.projection_kernel325  shows kernel(quotientProjection(G.carrier, cosetRelation(G, N)), G, G ⧸ N) = N326proof327  have subgroup := NormalSubgroup.subgroup with normal328  have equivalence := cosetRelation.equivalence with group, subgroup329  have subset := Subgroup.subset with subgroup330  ext x331  constructor332  . intro hx333    obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx334    rw quotientGroup.unit at vx335    have value := quotientProjection.value at G.carrier, cosetRelation(G, N), x with *336    have criterion := cosetRelation.class_eq_one_iff with group, subgroup, xIn337    apply criterion.forward338    cc339  . intro hx340    have xIn := subset with x, hx341    have value := quotientProjection.value at G.carrier, cosetRelation(G, N), x with *342    have criterion := cosetRelation.class_eq_one_iff with group, subgroup, xIn343    have equal := criterion.backward with hx344    apply kernel.of_value with xIn345    rw quotientGroup.unit346    cc347348-- Every normal subgroup is the kernel of a homomorphism.349theorem NormalSubgroup.is_kernel350  shows ∃ f, ∃ H, GroupHom(f, G, H) ∧ kernel(f, G, H) = N351proof352  have hom := quotientGroup.projection_hom with group, normal353  have same := quotientGroup.projection_kernel with group, normal354  refine ⟨quotientProjection(G.carrier, cosetRelation(G, N)), G ⧸ N, hom, same⟩355356end QuotientGroup357358section Extremes359variable (G : Set)360hypothesis group : Group(G)361362-- The quotient by the whole group has one element, and the quotient by363-- the trivial subgroup separates every pair of elements.364theorem quotientGroup.whole_class (x : G)365  shows ⟦x⟧[G.carrier, cosetRelation(G, G.carrier)] = ⟦G.one⟧[G.carrier, cosetRelation(G, G.carrier)]366proof367  have subgroup := Subgroup.whole with group368  have criterion := cosetRelation.class_eq_one_iff with group, subgroup, *369  exact criterion.backward with *370371theorem quotientGroup.trivial_class_injective (x y : G)372  requires equal : ⟦x⟧[G.carrier, cosetRelation(G, {G.one})] = ⟦y⟧[G.carrier, cosetRelation(G, {G.one})]373  shows x = y374proof375  have subgroup := Subgroup.trivial with group376  have criterion : ⟦x⟧[G.carrier, cosetRelation(G, {G.one})] = ⟦y⟧[G.carrier, cosetRelation(G, {G.one})] ↔377      x⁻¹ * y ∈ {G.one} := cosetRelation.class_eq_iff with *378  have member := criterion.forward with equal379  have vanishes := singleton.membership.forward with member380  have solved : x⁻¹ * y = G.one ↔ x = y := inv_mul_eq_one with *381  exact solved.forward with vanishes382383end Extremes384