Grace/Cumulus/Algebra/Group/FirstIsomorphism.g17

Open in Workbench Download source

Imports

Quotient · Isomorphism · Relation.QuotientMap

Declarations

Source

1-- Homomorphisms descend to quotients by normal subgroups of their kernel,2-- and the first isomorphism theorem: a group modulo the kernel of a3-- homomorphism is isomorphic to the image4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Group.FirstIsomorphism10import Quotient11import Isomorphism12import Relation.QuotientMap1314-- The map a homomorphism induces on the quotient by its kernel is written15-- inducedMap(f) under f : G →* H: the descent of f along the projection,16-- quotientMap(f, G.carrier, H.carrier, cosetRelation(G, ker(f))).17notation function "inducedMap(f)" => quotientMap(f, G.carrier, H.carrier, cosetRelation(G, ker(f))) via hypothesis GroupHom(f, G, H)1819section Descent20variable (f G H : Set)21hypothesis hom : f : G →* H2223theorem GroupHom.respects_coset_relation (N : Set)24  requires subgroup : Subgroup(N, G)25  requires killed : N ⊆ ker(f)26  shows Respects(f, G.carrier, cosetRelation(G, N))27proof28  have group := GroupHom.source with hom29  intros x hx y hy related30  have criterion : relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N := cosetRelation.relates with *31  have inKernel := killed with x⁻¹ * y, (criterion.forward with related)32  have images : f(x) = f(y) ↔ x⁻¹ * y ∈ ker(f) := GroupHom.apply_eq_iff with *33  exact images.backward with inKernel3435theorem GroupHom.reflects_kernel_relation (x y : G)36  requires equal : f(x) = f(y)37  shows relates(cosetRelation(G, ker(f)), x, y)38proof39  have group := GroupHom.source with hom40  have subgroup := GroupHom.kernel_subgroup with hom41  have criterion : relates(cosetRelation(G, ker(f)), x, y) ↔ x⁻¹ * y ∈ ker(f) :=42    cosetRelation.relates with *43  have images : f(x) = f(y) ↔ x⁻¹ * y ∈ ker(f) := GroupHom.apply_eq_iff with *44  exact criterion.backward with (images.forward with equal)4546-- The descended map is a homomorphism out of the quotient group.47theorem GroupHom.quotient_hom (N : Set)48  requires normal : NormalSubgroup(N, G)49  requires killed : N ⊆ ker(f)50  shows quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N)) : G ⧸ N →* H51proof52  have group := GroupHom.source with hom53  have target := GroupHom.target with hom54  have function := GroupHom.function with hom55  have subgroup := NormalSubgroup.subgroup with normal56  have equivalence := cosetRelation.equivalence with group, subgroup57  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed58  have mapped := quotientMap.function at f, G.carrier, H.carrier, cosetRelation(G, N) with *59  have qgroup := quotientGroup.group with group, normal60  have magma := IsGroup.magma with (Group.parts with group)61  have compatible := cosetRelation.mul_compatible with group, normal62  have descended : quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N)) : Group.carrier(G ⧸ N) → H.carrier63    rw quotientGroup.carrierOf64    exact mapped65  obtain ⟨source, target2, function2, preserves⟩ := hom66  apply GroupHom.mk with qgroup, target, descended67  intros X hX Y hY68  rw quotientGroup.carrierOf at hX69  rw quotientGroup.carrierOf at hY70  rw quotientGroup.operation71  exact quotientMap.binary with function, equivalence, respects, magma, compatible, preserves, hX, hY7273theorem GroupHom.quotient_factorization (N : Set)74  requires subgroup : Subgroup(N, G)75  requires killed : N ⊆ ker(f)76  shows compose(quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N)),77    quotientProjection(G.carrier, cosetRelation(G, N)), G.carrier,78    (G.carrier ⧸ cosetRelation(G, N)), H.carrier) = f79proof80  have group := GroupHom.source with hom81  have function := GroupHom.function with hom82  have equivalence := cosetRelation.equivalence with group, subgroup83  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed84  exact quotientMap.factorization with function, equivalence, respects8586theorem GroupHom.quotient_class (N : Set) (x : G)87  requires subgroup : Subgroup(N, G)88  requires killed : N ⊆ ker(f)89  shows quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N))(⟦x⟧[G.carrier, cosetRelation(G, N)]) = f(x)90proof91  have group := GroupHom.source with hom92  have function := GroupHom.function with hom93  have equivalence := cosetRelation.equivalence with group, subgroup94  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed95  exact quotientMap.class with function, equivalence, respects, *9697theorem GroupHom.quotient_unique (N g : Set)98  requires subgroup : Subgroup(N, G)99  requires killed : N ⊆ ker(f)100  requires candidate : g : (G.carrier ⧸ cosetRelation(G, N)) → H.carrier101  requires factors : ∀ x ∈ G, g(⟦x⟧[G.carrier, cosetRelation(G, N)]) = f(x)102  shows g = quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N))103proof104  have group := GroupHom.source with hom105  have function := GroupHom.function with hom106  have equivalence := cosetRelation.equivalence with group, subgroup107  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed108  exact quotientMap.unique with function, equivalence, respects, candidate, factors109110-- Modulo the kernel the descended map is injective.111theorem GroupHom.quotient_injective112  shows InjectiveBetween(inducedMap(f),113    Group.carrier(G ⧸ ker(f)), H.carrier)114proof115  have group := GroupHom.source with hom116  have function := GroupHom.function with hom117  have subgroup := GroupHom.kernel_subgroup with hom118  have killed := Subset.reflexive at ker(f)119  have equivalence := cosetRelation.equivalence with group, subgroup120  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed121  have reflects : ∀ x ∈ G, ∀ y ∈ G, f(x) = f(y) →122      relates(cosetRelation(G, ker(f)), x, y)123    intros x hx y hy equal124    exact GroupHom.reflects_kernel_relation with *125  rw quotientGroup.carrierOf126  exact quotientMap.injective with function, equivalence, respects, reflects127128theorem GroupHom.quotient_surjective (N : Set)129  requires subgroup : Subgroup(N, G)130  requires killed : N ⊆ ker(f)131  requires onto : SurjectiveBetween(f, G.carrier, H.carrier)132  shows SurjectiveBetween(quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N)),133    Group.carrier(G ⧸ N), H.carrier)134proof135  have group := GroupHom.source with hom136  have function := GroupHom.function with hom137  have equivalence := cosetRelation.equivalence with group, subgroup138  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed139  rw quotientGroup.carrierOf140  exact quotientMap.surjective with function, equivalence, respects, onto141142-- The first isomorphism theorem for a surjective homomorphism.143theorem GroupHom.first_isomorphism144  requires onto : SurjectiveBetween(f, G.carrier, H.carrier)145  shows inducedMap(f) : G ⧸ ker(f) ≃* H146proof147  have normal := GroupHom.kernel_normal with hom148  have subgroup := NormalSubgroup.subgroup with normal149  have killed := Subset.reflexive at ker(f)150  have quotientHom := GroupHom.quotient_hom with hom, normal, killed151  have injective := GroupHom.quotient_injective with hom152  have surjective := GroupHom.quotient_surjective with hom, subgroup, killed, onto153  have bijective : BijectiveBetween(inducedMap(f), Group.carrier(G ⧸ ker(f)), H.carrier)154    unfold BijectiveBetween155    exact ⟨injective, surjective⟩156  exact GroupIso.mk with quotientHom, bijective157158theorem GroupHom.quotient_isomorphic159  requires onto : SurjectiveBetween(f, G.carrier, H.carrier)160  shows G ⧸ ker(f) ≃* H161proof162  have iso := GroupHom.first_isomorphism with hom, onto163  witness inducedMap(f)164  exact iso165166theorem GroupHom.quotient_equipotent167  requires onto : SurjectiveBetween(f, G.carrier, H.carrier)168  shows Group.carrier(G ⧸ ker(f)) ≃ H.carrier169proof170  have iso := GroupHom.first_isomorphism with hom, onto171  exact GroupIso.equipotent with iso172173-- Without surjectivity, the quotient is isomorphic to the image.174theorem GroupHom.first_isomorphism_range175  shows quotientMap(f, G.carrier, functionImage(f, G.carrier, H.carrier), cosetRelation(G, ker(f))) :176    G ⧸ ker(f) ≃* subgroupGroup(H, functionImage(f, G.carrier, H.carrier))177proof178  have corestricted := GroupHom.corestrict with hom179  have onto := GroupHom.corestrict_surjective with hom180  have onto2 : SurjectiveBetween(f, G.carrier, Group.carrier(subgroupGroup(H, functionImage(f, G.carrier, H.carrier))))181    rw subgroupGroup.carrierOf182    exact onto183  have same : kernel(f, G, subgroupGroup(H, functionImage(f, G.carrier, H.carrier))) = kernel(f, G, H)184    ext x185    constructor186    . intro hx187      obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx188      rw subgroupGroup.unit at vx189      exact kernel.of_value with xIn, vx190    . intro hx191      obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx192      have value : f(x) = Group.one(subgroupGroup(H, functionImage(f, G.carrier, H.carrier)))193        rw subgroupGroup.unit194        exact vx195      exact kernel.of_value with xIn, value196  have iso := GroupHom.first_isomorphism with corestricted, onto2197  rw [same, subgroupGroup.carrierOf] at iso198  exact iso199200end Descent201