Grace/Cumulus/Algebra/Group/Isomorphism.g17

Open in Workbench Download source

Imports

Restricted · Cardinal.Finite

Declarations

Source

1-- Group isomorphisms f : G ≃* H and automorphisms: inverses and composites2-- of isomorphisms, isomorphism as an equivalence between groups, transfer3-- of commutativity, and conjugation as an inner automorphism4-- 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.Isomorphism10import Restricted11import Cardinal.Finite1213-- f : G ≃* H: a bijective homomorphism. G ≃* H: some isomorphism exists.14predicate GroupIso (f G H : Set) :=15  GroupHom(f, G, H) ∧ BijectiveBetween(f, G.carrier, H.carrier)1617predicate IsomorphicGroups (G H : Set) := ∃ f, GroupIso(f, G, H)1819predicate GroupAutomorphism (f G : Set) := GroupIso(f, G, G)2021notation guard "_ : _ ≃* _" => GroupIso22notation infix 50 "≃*" => IsomorphicGroups2324theorem GroupIso.mk (f G H : Set)25  requires hom : f : G →* H26  requires bijective : BijectiveBetween(f, G.carrier, H.carrier)27  shows f : G ≃* H28proof29  unfold GroupIso30  exact ⟨hom, bijective⟩3132section IsoLaws33variable (f G H : Set)34hypothesis iso : f : G ≃* H3536theorem GroupIso.hom37  shows f : G →* H38proof39  obtain ⟨hom, bijective⟩ := iso40  exact hom4142theorem GroupIso.bijective43  shows BijectiveBetween(f, G.carrier, H.carrier)44proof45  obtain ⟨hom, bijective⟩ := iso46  exact bijective4748theorem GroupIso.function49  shows f : G.carrier → H.carrier50proof51  have hom := GroupIso.hom with iso52  exact GroupHom.function with hom5354theorem GroupIso.injective55  shows InjectiveBetween(f, G.carrier, H.carrier)56proof57  have bijective := GroupIso.bijective with iso58  exact Bijective.injective with bijective5960theorem GroupIso.surjective61  shows SurjectiveBetween(f, G.carrier, H.carrier)62proof63  have bijective := GroupIso.bijective with iso64  exact Bijective.surjective with bijective6566theorem GroupIso.map_mul (a b : G)67  shows f(a * b) = f(a) * f(b)68proof69  have hom := GroupIso.hom with iso70  exact GroupHom.map_mul with *7172theorem GroupIso.equipotent73  shows G.carrier ≃ H.carrier74proof75  have bijective := GroupIso.bijective with iso76  witness f77  exact bijective7879theorem GroupIso.kernel_trivial80  shows ker(f) = {G.one}81proof82  have hom := GroupIso.hom with iso83  have injective := GroupIso.injective with iso84  have criterion := GroupHom.injective_iff_kernel_trivial with hom85  exact criterion.forward with injective8687theorem GroupIso.range88  shows functionImage(f, G.carrier, H.carrier) = H.carrier89proof90  have hom := GroupIso.hom with iso91  have surjective := GroupIso.surjective with iso92  have criterion := GroupHom.surjective_iff_range with hom93  exact criterion.forward with surjective9495-- The inverse of an isomorphism is an isomorphism.96theorem GroupIso.symm97  shows converse(f, G.carrier, H.carrier) : H ≃* G98proof99  have hom := GroupIso.hom with iso100  have group := GroupHom.source with hom101  have target := GroupHom.target with hom102  have bijective := GroupIso.bijective with iso103  have inverse := converse.function_of_bijective with bijective104  have inverseBijective := converse.bijective with bijective105  have inverseHom : converse(f, G.carrier, H.carrier) : H →* G106    apply GroupHom.mk with target, group, inverse107    intros y hy w hw108    have py := FunctionBetween.apply_closed with inverse, hy109    have pw := FunctionBetween.apply_closed with inverse, hw110    have fy := Bijective.apply_inverse with bijective, hy111    have fw := Bijective.apply_inverse with bijective, hw112    have closed : converse(f, G.carrier, H.carrier)(y) * converse(f, G.carrier, H.carrier)(w) ∈ G.carrier by typecheck113    have mapped : f(converse(f, G.carrier, H.carrier)(y) * converse(f, G.carrier, H.carrier)(w)) =114        f(converse(f, G.carrier, H.carrier)(y)) * f(converse(f, G.carrier, H.carrier)(w)) :=115      GroupHom.map_mul with *116    have recovered := Bijective.inverse_apply with bijective, closed117    cc118  exact GroupIso.mk with inverseHom, inverseBijective119120-- Commutativity transfers along an isomorphism.121theorem GroupIso.commutative122  requires commutative : Commutative(G.carrier, G.mul)123  shows Commutative(H.carrier, H.mul)124proof125  have function := GroupIso.function with iso126  have surjective := GroupIso.surjective with iso127  intros y hy w hw128  obtain ⟨x, hx, xEdge⟩ := surjective.right with y, hy129  obtain ⟨u, hu, uEdge⟩ := surjective.right with w, hw130  have yEq := FunctionBetween.apply_value with function, hx, xEdge131  have wEq := FunctionBetween.apply_value with function, hu, uEdge132  have first : f(x * u) = f(x) * f(u) := GroupIso.map_mul with *133  have second : f(u * x) = f(u) * f(x) := GroupIso.map_mul with *134  have swap := Commutative.law with commutative, hx, hu135  cc136137theorem GroupIso.abelian138  requires abelian : AbelianGroup(G)139  shows AbelianGroup(H)140proof141  have hom := GroupIso.hom with iso142  have target := GroupHom.target with hom143  have commutative := IsAbelianGroup.commutative with (AbelianGroup.parts with abelian)144  have transferred := GroupIso.commutative with iso, commutative145  unfold Basic.AbelianGroup146  exact ⟨target, transferred⟩147148end IsoLaws149150theorem GroupIso.id (G : Set)151  requires group : Group(G)152  shows identity(G.carrier) : G ≃* G153proof154  have hom := GroupHom.id with group155  have bijective := identity.bijective at G.carrier156  exact GroupIso.mk with hom, bijective157158theorem GroupIso.trans (f g G H K : Set)159  requires first : f : G ≃* H160  requires second : g : H ≃* K161  shows compose(g, f, G.carrier, H.carrier, K.carrier) : G ≃* K162proof163  have hom := GroupHom.comp with (GroupIso.hom with first), (GroupIso.hom with second)164  have bijective := compose.bijective with (GroupIso.bijective with first), (GroupIso.bijective with second)165  exact GroupIso.mk with hom, bijective166167-- An injective homomorphism is an isomorphism onto its image.168theorem GroupHom.iso_onto_range (f G H : Set)169  requires hom : f : G →* H170  requires injective : InjectiveBetween(f, G.carrier, H.carrier)171  shows f : G ≃* subgroupGroup(H, functionImage(f, G.carrier, H.carrier))172proof173  have corestricted := GroupHom.corestrict with hom174  have injectiveImage := Injective.corestrict with injective175  have surjectiveImage := GroupHom.corestrict_surjective with hom176  have bijective : BijectiveBetween(f, G.carrier, Group.carrier(subgroupGroup(H, functionImage(f, G.carrier, H.carrier))))177    rw subgroupGroup.carrierOf178    exact ⟨injectiveImage, surjectiveImage⟩179  exact GroupIso.mk with corestricted, bijective180181theorem IsomorphicGroups.refl (G : Set)182  requires group : Group(G)183  shows G ≃* G184proof185  have iso := GroupIso.id with group186  witness identity(G.carrier)187  exact iso188189theorem IsomorphicGroups.symm (G H : Set)190  requires isomorphic : G ≃* H191  shows H ≃* G192proof193  obtain ⟨f, iso⟩ := isomorphic194  have inverse := GroupIso.symm with iso195  witness converse(f, G.carrier, H.carrier)196  exact inverse197198theorem IsomorphicGroups.trans (G H K : Set)199  requires first : G ≃* H200  requires second : H ≃* K201  shows G ≃* K202proof203  obtain ⟨f, isoF⟩ := first204  obtain ⟨g, isoG⟩ := second205  have composed := GroupIso.trans with isoF, isoG206  witness compose(g, f, G.carrier, H.carrier, K.carrier)207  exact composed208209theorem IsomorphicGroups.equipotent (G H : Set)210  requires isomorphic : G ≃* H211  shows G.carrier ≃ H.carrier212proof213  obtain ⟨f, iso⟩ := isomorphic214  exact GroupIso.equipotent with iso215216theorem IsomorphicGroups.abelian (G H : Set)217  requires isomorphic : G ≃* H218  requires abelian : AbelianGroup(G)219  shows AbelianGroup(H)220proof221  obtain ⟨f, iso⟩ := isomorphic222  exact GroupIso.abelian with iso, abelian223224-- Automorphisms.225theorem GroupAutomorphism.iso (f G : Set)226  requires automorphism : GroupAutomorphism(f, G)227  shows f : G ≃* G228proof229  exact automorphism230231theorem GroupAutomorphism.id (G : Set)232  requires group : Group(G)233  shows GroupAutomorphism(identity(G.carrier), G)234proof235  unfold GroupAutomorphism236  exact GroupIso.id with group237238theorem GroupAutomorphism.symm (f G : Set)239  requires automorphism : GroupAutomorphism(f, G)240  shows GroupAutomorphism(converse(f, G.carrier, G.carrier), G)241proof242  have iso := GroupAutomorphism.iso with automorphism243  unfold GroupAutomorphism244  exact GroupIso.symm with iso245246theorem GroupAutomorphism.trans (f g G : Set)247  requires first : GroupAutomorphism(f, G)248  requires second : GroupAutomorphism(g, G)249  shows GroupAutomorphism(compose(g, f, G.carrier, G.carrier, G.carrier), G)250proof251  have isoF := GroupAutomorphism.iso with first252  have isoG := GroupAutomorphism.iso with second253  unfold GroupAutomorphism254  exact GroupIso.trans with isoF, isoG255256section Automorphisms257variable (G : Set)258hypothesis group : Group(G)259260theorem conjugation.automorphism (g : G)261  shows GroupAutomorphism(conjugation(G, g), G)262proof263  have hom := conjugation.hom with *264  have bijective := conjugation.bijective with *265  unfold GroupAutomorphism266  exact GroupIso.mk with hom, bijective267268theorem GroupAutomorphism.map_one (f : Set)269  requires automorphism : GroupAutomorphism(f, G)270  shows f(G.one) = G.one271proof272  have hom := GroupIso.hom with (GroupAutomorphism.iso with automorphism)273  exact GroupHom.map_one with hom274275theorem GroupAutomorphism.image_subgroup (f H : Set)276  requires automorphism : GroupAutomorphism(f, G)277  requires subgroup : Subgroup(H, G)278  shows Subgroup(functionImage(f, H, G.carrier), G)279proof280  have hom := GroupIso.hom with (GroupAutomorphism.iso with automorphism)281  exact GroupHom.image_subgroup with hom, subgroup282283theorem GroupAutomorphism.image_normal (f N : Set)284  requires automorphism : GroupAutomorphism(f, G)285  requires normal : NormalSubgroup(N, G)286  shows NormalSubgroup(functionImage(f, N, G.carrier), G)287proof288  have iso := GroupAutomorphism.iso with automorphism289  have hom := GroupIso.hom with iso290  have surjective := GroupIso.surjective with iso291  exact NormalSubgroup.image_of_surjective with hom, surjective, normal292293end Automorphisms294