Grace/Cumulus/Algebra/Group/Restricted.g17

Open in Workbench Download source

Imports

Normal · Algebra.Restriction

Declarations

Source

1-- A subgroup as a group of its own, with the operations restricted to it;2-- the inclusion of a subgroup is a homomorphism, and homomorphisms restrict3-- to subgroups and corestrict to their images4-- 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.Restricted10import Normal11import Algebra.Restriction1213-- The group on a subgroup H of G: the carrier H with the operation and14-- inverse of G restricted to it.15def subgroupGroup (G H : Set) : Set :=16  Group.mk(H, restrict(G.mul, H × H), G.one, restrict(G.inv, H))1718theorem subgroupGroup.carrierOf (G H : Set)19  shows Group.carrier(subgroupGroup(G, H)) = H20proof21  simp [subgroupGroup, Group.mk.carrier]2223theorem subgroupGroup.operation (G H : Set)24  shows Group.mul(subgroupGroup(G, H)) = restrict(G.mul, H × H)25proof26  simp [subgroupGroup, Group.mk.mul]2728theorem subgroupGroup.unit (G H : Set)29  shows Group.one(subgroupGroup(G, H)) = G.one30proof31  simp [subgroupGroup, Group.mk.one]3233theorem subgroupGroup.inverse (G H : Set)34  shows Group.inv(subgroupGroup(G, H)) = restrict(G.inv, H)35proof36  simp [subgroupGroup, Group.mk.inv]3738section Restricted39variable (G H : Set)40hypothesis group : Group(G)41hypothesis subgroup : Subgroup(H, G)4243theorem Subgroup.closed_binary44  shows ClosedBinary(H, G.mul)45proof46  intros x hx y hy47  exact Subgroup.mul_mem with *4849theorem Subgroup.closed_unary50  shows ClosedUnary(H, G.inv)51proof52  intros x hx53  exact Subgroup.inv_mem with *5455theorem subgroupGroup.mul (h k : H)56  shows Group.mul(subgroupGroup(G, H))(h, k) = h * k57proof58  have magma := IsGroup.magma with (Group.parts with group)59  have subset := Subgroup.subset with subgroup60  have closed := Subgroup.closed_binary with group, subgroup61  rw subgroupGroup.operation62  exact restrictBinary.value with magma, subset, closed, *6364theorem subgroupGroup.inverse_value (h : H)65  shows Group.inv(subgroupGroup(G, H))(h) = h⁻¹66proof67  have function := Group.inverse_function with group68  have subset := Subgroup.subset with subgroup69  have closed := Subgroup.closed_unary with group, subgroup70  rw subgroupGroup.inverse71  exact restrictUnary.value with function, subset, closed, *7273theorem Subgroup.restricted_group74  shows IsGroup(H, restrict(G.mul, H × H), G.one, restrict(G.inv, H))75proof76  have parts := Group.parts with group77  have magma := IsGroup.magma with parts78  have monoid := IsGroup.monoid with parts79  have associative := IsMonoid.associative with monoid80  have identity := IsMonoid.identity with monoid81  have inverse := IsGroup.inverse with parts82  have negation := inverse.left83  have subset := Subgroup.subset with subgroup84  have unitIn : G.one ∈ H := Subgroup.one_mem with *85  have opClosed := Subgroup.closed_binary with group, subgroup86  have invClosed := Subgroup.closed_unary with group, subgroup87  have function := restrictBinary.function with magma, subset, opClosed88  have rMagma : IsMagma(H, restrict(G.mul, H × H)) by exact function89  have rAssociative := restrictBinary.associative with magma, subset, opClosed, associative90  have rIdentity := restrictBinary.identity with magma, subset, opClosed, identity, unitIn91  have rInverse := restrictUnary.inverse with magma, negation, subset, opClosed, invClosed, inverse92  simp [IsGroup, IsMonoid, IsSemigroup]9394theorem subgroupGroup.group95  shows Group(subgroupGroup(G, H))96proof97  have restricted := Subgroup.restricted_group with group, subgroup98  unfold subgroupGroup99  exact Group.of_parts with restricted100101theorem subgroupGroup.abelian102  requires abelian : AbelianGroup(G)103  shows AbelianGroup(subgroupGroup(G, H))104proof105  have commutative := IsAbelianGroup.commutative with (AbelianGroup.parts with abelian)106  have magma := IsGroup.magma with (Group.parts with group)107  have subset := Subgroup.subset with subgroup108  have opClosed := Subgroup.closed_binary with group, subgroup109  have restricted := Subgroup.restricted_group with group, subgroup110  have rCommutative := restrictBinary.commutative with magma, subset, opClosed, commutative111  unfold subgroupGroup112  apply AbelianGroup.of_parts113  unfold IsAbelianGroup114  exact ⟨restricted, rCommutative⟩115116-- The inclusion of a subgroup is an injective homomorphism.117theorem Subgroup.inclusion_hom118  shows identity(H) : subgroupGroup(G, H) →* G119proof120  have subgroupGroupIs := subgroupGroup.group with group, subgroup121  have subset := Subgroup.subset with subgroup122  have function : identity(H) : Group.carrier(subgroupGroup(G, H)) → G.carrier123    rw subgroupGroup.carrierOf124    exact identity.inclusion with subset125  apply GroupHom.mk with subgroupGroupIs, group, function126  intros x hx y hy127  rw subgroupGroup.carrierOf at hx128  rw subgroupGroup.carrierOf at hy129  have restricted : Group.mul(subgroupGroup(G, H))(x, y) = G.mul(x, y) := subgroupGroup.mul with *130  have vx := identity.apply with hx131  have vy := identity.apply with hy132  have closed : G.mul(x, y) ∈ H := Subgroup.mul_mem with *133  have output := identity.apply with closed134  rw [restricted, output, vx, vy]135  rfl136137theorem Subgroup.inclusion_injective138  shows InjectiveBetween(identity(H), H, G.carrier)139proof140  have subset := Subgroup.subset with subgroup141  have function := identity.inclusion with subset142  constructor143  . exact function144  . intros x hx y hy z hz hxz hyz145    have vx := identity.apply with hx146    have vy := identity.apply with hy147    have ex := FunctionBetween.apply_value with function, hx, hxz148    have ey := FunctionBetween.apply_value with function, hy, hyz149    cc150151end Restricted152153section RestrictedHoms154variable (f G H : Set)155hypothesis hom : f : G →* H156157-- A homomorphism restricted to a subgroup, as a homomorphism out of the158-- subgroup's group.159theorem GroupHom.restrict (K : Set)160  requires subgroup : Subgroup(K, G)161  shows restrict(f, K) : subgroupGroup(G, K) →* H162proof163  have group := GroupHom.source with hom164  have target := GroupHom.target with hom165  have function := GroupHom.function with hom166  have subset := Subgroup.subset with subgroup167  have subgroupGroupIs := subgroupGroup.group with group, subgroup168  have restricted := restrict.domain_function with function, subset169  have restrictedFunction : restrict(f, K) : Group.carrier(subgroupGroup(G, K)) → H.carrier170    rw subgroupGroup.carrierOf171    exact restricted172  apply GroupHom.mk with subgroupGroupIs, target, restrictedFunction173  intros x hx y hy174  rw subgroupGroup.carrierOf at hx175  rw subgroupGroup.carrierOf at hy176  have xIn : x ∈ G := Subgroup.mem_carrier with *177  have yIn : y ∈ G := Subgroup.mem_carrier with *178  have closed : G.mul(x, y) ∈ K := Subgroup.mul_mem with *179  have mulValue : Group.mul(subgroupGroup(G, K))(x, y) = G.mul(x, y) := subgroupGroup.mul with *180  have vx := restrict.domain_apply with function, subset, hx181  have vy := restrict.domain_apply with function, subset, hy182  have output := restrict.domain_apply with function, subset, closed183  have preserved : f(G.mul(x, y)) = f(x) * f(y) := GroupHom.map_mul with *184  rw [mulValue, output, vx, vy]185  exact preserved186187-- The corestriction of a homomorphism to its image.188theorem GroupHom.corestrict189  shows f : G →* subgroupGroup(H, functionImage(f, G.carrier, H.carrier))190proof191  have group := GroupHom.source with hom192  have target := GroupHom.target with hom193  have function := GroupHom.function with hom194  have rangeSubgroup := GroupHom.range_subgroup with hom195  have rangeGroup := subgroupGroup.group with target, rangeSubgroup196  have corestricted : f : G.carrier → Group.carrier(subgroupGroup(H, functionImage(f, G.carrier, H.carrier)))197    rw subgroupGroup.carrierOf198    exact functionImage.corestrict with function199  apply GroupHom.mk with group, rangeGroup, corestricted200  intros x hx y hy201  have fx := functionImage.value with function, hx202  have fy := functionImage.value with function, hy203  have mulValue : Group.mul(subgroupGroup(H, functionImage(f, G.carrier, H.carrier)))(f(x), f(y)) =204      H.mul(f(x), f(y)) := subgroupGroup.mul with *205  have preserved : f(x * y) = H.mul(f(x), f(y)) := GroupHom.map_mul with *206  rw mulValue207  exact preserved208209theorem GroupHom.range_group210  shows Group(subgroupGroup(H, functionImage(f, G.carrier, H.carrier)))211proof212  have target := GroupHom.target with hom213  have rangeSubgroup := GroupHom.range_subgroup with hom214  exact subgroupGroup.group with target, rangeSubgroup215216theorem GroupHom.image_factorization217  shows compose(identity(functionImage(f, G.carrier, H.carrier)), f, G.carrier,218    functionImage(f, G.carrier, H.carrier), H.carrier) = f219proof220  have function := GroupHom.function with hom221  have corestricted := functionImage.corestrict with function222  have subset := functionImage.subset at f, G.carrier, H.carrier223  have inclusion := identity.inclusion with subset224  have composed := compose.function with corestricted, inclusion225  apply FunctionBetween.ext with composed, function226  intros x hx227  have fx := functionImage.value with function, hx228  have value := compose.apply at identity(functionImage(f, G.carrier, H.carrier)), f, G.carrier, functionImage(f, G.carrier, H.carrier), H.carrier, x with *229  have included := identity.apply with fx230  cc231232-- The kernel of a restricted homomorphism is the restricted kernel.233theorem GroupHom.kernel_restrict (K : Set)234  requires subgroup : Subgroup(K, G)235  shows kernel(restrict(f, K), subgroupGroup(G, K), H) = ker(f) ∩ K236proof237  have function := GroupHom.function with hom238  have subset := Subgroup.subset with subgroup239  ext x240  constructor241  . intro hx242    obtain ⟨xK, vx⟩ := kernel.membership.forward with hx243    rw subgroupGroup.carrierOf at xK244    have xIn := subset with x, xK245    have restricted := restrict.domain_apply with function, subset, xK246    have vanishes : f(x) = H.one by cc247    have inKernel := kernel.of_value with xIn, vanishes248    exact intersection.membership.backward with ⟨inKernel, xK⟩249  . intro hx250    obtain ⟨inKernel, xK⟩ := intersection.membership.forward with hx251    have vx := kernel.value with inKernel252    have restricted := restrict.domain_apply with function, subset, xK253    have vanishes : restrict(f, K)(x) = H.one by cc254    have xIn : x ∈ Group.carrier(subgroupGroup(G, K))255      rw subgroupGroup.carrierOf256      exact xK257    exact kernel.of_value with xIn, vanishes258259end RestrictedHoms260