Grace/Cumulus/Algebra/Group/Homomorphism.g17

Open in Workbench Download source

Imports

Pow

Declarations

Source

1-- Group homomorphisms f : G →* H: maps preserving the operation, hence the2-- unit, inverses, and powers; identity, constant, and composite3-- homomorphisms4-- 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.Homomorphism10import Pow1112-- f : G →* H: a function between the carriers preserving the operation;13-- the unit and inverse laws follow. The form is a transparent guard, so a14-- hypothesis f : G →* H also supplies the groups G and H, their operations15-- a * b, and the binders (a : G) and (b : H).16predicate GroupHom (f G H : Set) :=17  Group(G) ∧ Group(H) ∧ (f : G.carrier → H.carrier) ∧18  (∀ x y ∈ G.carrier, f(x * y) = f(x) * f(y))1920notation guard "_ : _ →* _" => GroupHom2122theorem GroupHom.mk (f G H : Set)23  requires source : Group(G)24  requires target : Group(H)25  requires function : f : G.carrier → H.carrier26  requires preserves : ∀ x y ∈ G.carrier, f(x * y) = f(x) * f(y)27  shows f : G →* H28proof29  unfold GroupHom30  refine ⟨source, target, function, preserves⟩3132section HomLaws33variable (f G H : Set)34hypothesis hom : f : G →* H3536theorem GroupHom.source37  shows Group(G)38proof39  obtain ⟨source, rest⟩ := hom40  exact source4142theorem GroupHom.target43  shows Group(H)44proof45  obtain ⟨source, target, rest⟩ := hom46  exact target4748theorem GroupHom.function49  shows f : G.carrier → H.carrier50proof51  obtain ⟨source, target, function, preserves⟩ := hom52  exact function5354theorem GroupHom.map_mul (a b : G)55  shows f(a * b) = f(a) * f(b)56proof57  obtain ⟨source, target, function, preserves⟩ := hom58  have aIn : a ∈ G by assumption59  have bIn : b ∈ G by assumption60  exact preserves with a, aIn, b, bIn6162instance GroupHom.map_mem (a : G)63  shows f(a) ∈ H64proof65  have function := GroupHom.function with hom66  exact FunctionBetween.apply_closed with function, *6768theorem GroupHom.map_one69  shows f(G.one) = H.one70proof71  have group := GroupHom.source with hom72  have target := GroupHom.target with hom73  have preserved : f(G.one * G.one) = f(G.one) * f(G.one) := GroupHom.map_mul with *74  rw mul_one at preserved75  have criterion : f(G.one) * f(G.one) = f(G.one) ↔ f(G.one) = H.one := mul_self_eq_self with *76  symm at preserved77  exact criterion.forward with preserved7879theorem GroupHom.map_inv (a : G)80  shows f(a⁻¹) = f(a)⁻¹81proof82  have product : f(a) * f(a⁻¹) = H.one83    rw [← GroupHom.map_mul, Group.mul_inv, GroupHom.map_one]84    rfl85  exact eq_inv_of_mul_eq_one_right with *8687theorem GroupHom.map_mul_inv (a b : G)88  shows f(a * b⁻¹) = f(a) * f(b)⁻¹89proof90  rw [GroupHom.map_mul, GroupHom.map_inv]91  rfl9293theorem GroupHom.map_inv_mul (a b : G)94  shows f(a⁻¹ * b) = f(a)⁻¹ * f(b)95proof96  rw [GroupHom.map_mul, GroupHom.map_inv]97  rfl9899theorem GroupHom.map_pow (a : G) (n : Nat)100  shows f(a ^ n) = f(a) ^ n101proof102  have group := GroupHom.source with hom103  have target := GroupHom.target with hom104  induction n105  | zero =>106    rw [pow_zero, pow_zero, GroupHom.map_one]107    rfl108  | succ(k) using ih =>109    rw [← add.right_one, pow_succ, pow_succ, GroupHom.map_mul, ih]110    rfl111112theorem GroupHom.map_inv_eq_one (a : G)113  requires vanishes : f(a) = H.one114  shows f(a⁻¹) = H.one115proof116  rw [GroupHom.map_inv, vanishes, inv_one]117  rfl118119theorem GroupHom.ext (g : Set)120  requires hom2 : g : G →* H121  requires same : ∀ x ∈ G, f(x) = g(x)122  shows f = g123proof124  have fFunction := GroupHom.function with hom125  have gFunction := GroupHom.function with hom2126  exact FunctionBetween.ext with fFunction, gFunction, same127128theorem GroupHom.id_comp129  shows compose(identity(H.carrier), f, G.carrier, H.carrier, H.carrier) = f130proof131  have function := GroupHom.function with hom132  exact compose.identity_left with function133134theorem GroupHom.comp_id135  shows compose(f, identity(G.carrier), G.carrier, G.carrier, H.carrier) = f136proof137  have function := GroupHom.function with hom138  exact compose.identity_right with function139140end HomLaws141142theorem GroupHom.id (G : Set)143  requires group : Group(G)144  shows identity(G.carrier) : G →* G145proof146  have function := identity.function at G.carrier147  apply GroupHom.mk with group, group, function148  intros x hx y hy149  have vx := identity.apply with hx150  have vy := identity.apply with hy151  have closed : x * y ∈ G.carrier by typecheck152  have output := identity.apply with closed153  rw [vx, vy]154  exact output155156theorem GroupHom.const (G H : Set)157  requires group : Group(G)158  requires target : Group(H)159  shows constantFunction(G.carrier, H.carrier, H.one) : G →* H160proof161  have unitIn : H.one ∈ H.carrier := Group.one_mem with *162  have function := constantFunction.function at G.carrier, H.carrier, H.one with unitIn163  apply GroupHom.mk with group, target, function164  intros x hx y hy165  have vx := constantFunction.apply with hx, unitIn166  have vy := constantFunction.apply with hy, unitIn167  have closed : x * y ∈ G.carrier by typecheck168  have output := constantFunction.apply with closed, unitIn169  rw [vx, vy, output, one_mul]170  rfl171172theorem GroupHom.comp (f g G H K : Set)173  requires first : f : G →* H174  requires second : g : H →* K175  shows compose(g, f, G.carrier, H.carrier, K.carrier) : G →* K176proof177  have source := GroupHom.source with first178  have target := GroupHom.target with second179  have fFunction := GroupHom.function with first180  have gFunction := GroupHom.function with second181  have function := compose.function with fFunction, gFunction182  apply GroupHom.mk with source, target, function183  intros x hx y hy184  have fx : f(x) ∈ H.carrier by typecheck185  have fy : f(y) ∈ H.carrier by typecheck186  have fMul : f(x * y) = f(x) * f(y) := GroupHom.map_mul with *187  have gMul : g(f(x) * f(y)) = g(f(x)) * g(f(y)) := GroupHom.map_mul with *188  have vx := compose.apply at g, f, G.carrier, H.carrier, K.carrier, x with *189  have vy := compose.apply at g, f, G.carrier, H.carrier, K.carrier, y with *190  have closed : x * y ∈ G.carrier by typecheck191  have output := compose.apply at g, f, G.carrier, H.carrier, K.carrier, x * y with *192  cc193