Grace/Cumulus/Algebra/Group/Product.g17

Open in Workbench Download source

Imports

Normal · Set.Function.Projection

Declarations

Source

1-- The direct product of two groups on the product of their carriers,2-- with the componentwise operation: it is a group, abelian when both3-- factors are, the projections are surjective homomorphisms, and each4-- factor embeds as a normal subgroup5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Group.Product11import Normal12import Set.Function.Projection1314-- The componentwise operation as a function graph on (A × B) × (A × B).15def productOp (A op B op2 : Set) : Set :=16  { q ∈ ((A × B) × (A × B)) × (A × B) |17    ∃ a ∈ A, ∃ b ∈ B, ∃ c ∈ A, ∃ d ∈ B,18      q = (((a, b), (c, d)) ↦ (op(a, c), op2(b, d))) }1920-- The componentwise inverse as a function graph on A × B.21def productInv (A inv B inv2 : Set) : Set :=22  { q ∈ (A × B) × (A × B) | ∃ a ∈ A, ∃ b ∈ B, q = ((a, b) ↦ (inv(a), inv2(b))) }2324-- The direct product of two bundled groups.25def productGroup (G H : Set) : Set :=26  Group.mk(G.carrier × H.carrier, productOp(G.carrier, G.mul, H.carrier, H.mul),27    (G.one, H.one), productInv(G.carrier, G.inv, H.carrier, H.inv))2829theorem productGroup.carrierOf (G H : Set)30  shows Group.carrier(productGroup(G, H)) = G.carrier × H.carrier31proof32  simp [productGroup, Group.mk.carrier]3334theorem productGroup.operation (G H : Set)35  shows Group.mul(productGroup(G, H)) = productOp(G.carrier, G.mul, H.carrier, H.mul)36proof37  simp [productGroup, Group.mk.mul]3839theorem productGroup.unit (G H : Set)40  shows Group.one(productGroup(G, H)) = (G.one, H.one)41proof42  simp [productGroup, Group.mk.one]4344theorem productGroup.inverse (G H : Set)45  shows Group.inv(productGroup(G, H)) = productInv(G.carrier, G.inv, H.carrier, H.inv)46proof47  simp [productGroup, Group.mk.inv]4849theorem productOp.relates (A op B op2 a b c d : Set)50  requires magma : IsMagma(A, op)51  requires magma2 : IsMagma(B, op2)52  requires ha : a ∈ A53  requires hb : b ∈ B54  requires hc : c ∈ A55  requires hd : d ∈ B56  shows relates(productOp(A, op, B, op2), ((a, b), (c, d)), (op(a, c), op2(b, d)))57proof58  have ab := product.pair at a, b, A, B with *59  have cd := product.pair at c, d, A, B with *60  have input := product.pair at (a, b), (c, d), A × B, A × B with *61  have first := IsMagma.closed with magma, ha, hc62  have second := IsMagma.closed with magma2, hb, hd63  have output := product.pair at op(a, c), op2(b, d), A, B with *64  have bounded := product.pair at ((a, b), (c, d)), (op(a, c), op2(b, d)), (A × B) × (A × B), A × B with *65  unfold relates66  apply productOp.membership.backward67  refine ⟨bounded, a, ha, b, hb, c, hc, d, hd, rfl⟩6869theorem productOp.function (A op B op2 : Set)70  requires magma : IsMagma(A, op)71  requires magma2 : IsMagma(B, op2)72  shows productOp(A, op, B, op2) : (A × B) × (A × B) → A × B73proof74  unfold FunctionBetween75  refine ⟨?_, ?_, ?_⟩76  . intros q hq77    have parts := productOp.membership.forward with hq78    exact parts.left79  . intros p y edge z edge280    unfold relates at edge81    unfold relates at edge282    obtain ⟨bounded, a, ha, b, hb, c, hc, d, hd, shape⟩ := productOp.membership.forward with edge83    obtain ⟨bounded2, a2, ha2, b2, hb2, c2, hc2, d2, hd2, shape2⟩ := productOp.membership.forward with edge284    have outer := orderedPair.injective with shape85    have outer2 := orderedPair.injective with shape286    have inputs : ((a, b), (c, d)) = ((a2, b2), (c2, d2)) by cc87    have halves := orderedPair.injective with inputs88    have left := orderedPair.injective with halves.left89    have right := orderedPair.injective with halves.right90    cc91  . intros p hp92    obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with hp93    obtain ⟨boundU, a, ha, b, hb, uShape⟩ := product.membership.forward with hu94    obtain ⟨boundV, c, hc, d, hd, vShape⟩ := product.membership.forward with hv95    have first := IsMagma.closed with magma, ha, hc96    have second := IsMagma.closed with magma2, hb, hd97    have output := product.pair at op(a, c), op2(b, d), A, B with *98    have edge := productOp.relates with magma, magma2, ha, hb, hc, hd99    refine ⟨(op(a, c), op2(b, d)), output, ?_⟩100    rw [shape, uShape, vShape]101    exact edge102103theorem productOp.value (A op B op2 a b c d : Set)104  requires magma : IsMagma(A, op)105  requires magma2 : IsMagma(B, op2)106  requires ha : a ∈ A107  requires hb : b ∈ B108  requires hc : c ∈ A109  requires hd : d ∈ B110  shows (productOp(A, op, B, op2))((a, b), (c, d)) = (op(a, c), op2(b, d))111proof112  have function := productOp.function with magma, magma2113  have edge := productOp.relates with magma, magma2, ha, hb, hc, hd114  have ab := product.pair at a, b, A, B with *115  have cd := product.pair at c, d, A, B with *116  have input := product.pair at (a, b), (c, d), A × B, A × B with *117  have value := FunctionBetween.apply_value with function, input, edge118  have called : (productOp(A, op, B, op2))((a, b), (c, d)) =119      productOp(A, op, B, op2)(((a, b), (c, d)))120    unfold call2121    rfl122  rw called123  exact value124125theorem productInv.relates (A inv B inv2 a b : Set)126  requires function : inv : A → A127  requires function2 : inv2 : B → B128  requires ha : a ∈ A129  requires hb : b ∈ B130  shows relates(productInv(A, inv, B, inv2), (a, b), (inv(a), inv2(b)))131proof132  have ab := product.pair at a, b, A, B with *133  have invA := FunctionBetween.apply_closed with function, ha134  have invB := FunctionBetween.apply_closed with function2, hb135  have output := product.pair at inv(a), inv2(b), A, B with *136  have bounded := product.pair at (a, b), (inv(a), inv2(b)), A × B, A × B with *137  unfold relates138  apply productInv.membership.backward139  refine ⟨bounded, a, ha, b, hb, rfl⟩140141theorem productInv.function (A inv B inv2 : Set)142  requires function : inv : A → A143  requires function2 : inv2 : B → B144  shows productInv(A, inv, B, inv2) : A × B → A × B145proof146  unfold FunctionBetween147  refine ⟨?_, ?_, ?_⟩148  . intros q hq149    have parts := productInv.membership.forward with hq150    exact parts.left151  . intros p y edge z edge2152    unfold relates at edge153    unfold relates at edge2154    obtain ⟨bounded, a, ha, b, hb, shape⟩ := productInv.membership.forward with edge155    obtain ⟨bounded2, a2, ha2, b2, hb2, shape2⟩ := productInv.membership.forward with edge2156    have outer := orderedPair.injective with shape157    have outer2 := orderedPair.injective with shape2158    have inputs : (a, b) = (a2, b2) by cc159    have halves := orderedPair.injective with inputs160    cc161  . intros p hp162    obtain ⟨bound, a, ha, b, hb, shape⟩ := product.membership.forward with hp163    have invA := FunctionBetween.apply_closed with function, ha164    have invB := FunctionBetween.apply_closed with function2, hb165    have output := product.pair at inv(a), inv2(b), A, B with *166    have edge := productInv.relates with function, function2, ha, hb167    refine ⟨(inv(a), inv2(b)), output, ?_⟩168    rw shape169    exact edge170171theorem productInv.value (A inv B inv2 a b : Set)172  requires function : inv : A → A173  requires function2 : inv2 : B → B174  requires ha : a ∈ A175  requires hb : b ∈ B176  shows (productInv(A, inv, B, inv2))((a, b)) = (inv(a), inv2(b))177proof178  have graph := productInv.function with function, function2179  have edge := productInv.relates with function, function2, ha, hb180  have ab := product.pair at a, b, A, B with *181  exact FunctionBetween.apply_value with graph, ab, edge182183section ProductGroup184variable (G H : Set)185hypothesis group : Group(G)186hypothesis group2 : Group(H)187188theorem productGroup.mul (a c : G) (b d : H)189  shows Group.mul(productGroup(G, H))((a, b), (c, d)) = (a * c, b * d)190proof191  have magma := IsGroup.magma with (Group.parts with group)192  have magma2 := IsGroup.magma with (Group.parts with group2)193  rw productGroup.operation194  exact productOp.value with magma, magma2, *195196theorem productGroup.inv_value (a : G) (b : H)197  shows Group.inv(productGroup(G, H))((a, b)) = (a⁻¹, b⁻¹)198proof199  have function := Group.inverse_function with group200  have function2 := Group.inverse_function with group2201  rw productGroup.inverse202  exact productInv.value with function, function2, *203204-- The direct product is a group.205theorem productGroup.group206  shows Group(productGroup(G, H))207proof208  have magma := IsGroup.magma with (Group.parts with group)209  have magma2 := IsGroup.magma with (Group.parts with group2)210  have invFunction := Group.inverse_function with group211  have invFunction2 := Group.inverse_function with group2212  have unitIn : G.one ∈ G := Group.one_mem with *213  have unitIn2 : H.one ∈ H := Group.one_mem with *214  have opFunction := productOp.function with magma, magma2215  have pMagma : IsMagma(G.carrier × H.carrier, productOp(G.carrier, G.mul, H.carrier, H.mul)) by exact opFunction216  have pAssociative : Associative(G.carrier × H.carrier, productOp(G.carrier, G.mul, H.carrier, H.mul))217    intros X hX Y hY Z hZ218    obtain ⟨boundX, a, ha, b, hb, xShape⟩ := product.membership.forward with hX219    obtain ⟨boundY, c, hc, d, hd, yShape⟩ := product.membership.forward with hY220    obtain ⟨boundZ, e, he, f, hf, zShape⟩ := product.membership.forward with hZ221    have ac : a * c ∈ G by typecheck222    have bd : b * d ∈ H by typecheck223    have ce : c * e ∈ G by typecheck224    have df : d * f ∈ H by typecheck225    have xy := productOp.value with magma, magma2, ha, hb, hc, hd226    have yz := productOp.value with magma, magma2, hc, hd, he, hf227    have left := productOp.value with magma, magma2, ac, bd, he, hf228    have right := productOp.value with magma, magma2, ha, hb, ce, df229    have assocA : a * c * e = a * (c * e) := mul_assoc with *230    have assocB : b * d * f = b * (d * f) := mul_assoc with *231    rw [xShape, yShape, zShape]232    cc233  have pIdentity : Identity(G.carrier × H.carrier, productOp(G.carrier, G.mul, H.carrier, H.mul), (G.one, H.one))234    have unitPair := product.pair at G.one, H.one, G.carrier, H.carrier with *235    unfold Identity236    refine ⟨unitPair, ?_⟩237    intros X hX238    obtain ⟨boundX, a, ha, b, hb, xShape⟩ := product.membership.forward with hX239    have leftA : G.one * a = a := one_mul with *240    have leftB : H.one * b = b := one_mul with *241    have rightA : a * G.one = a := mul_one with *242    have rightB : b * H.one = b := mul_one with *243    have left := productOp.value with magma, magma2, unitIn, unitIn2, ha, hb244    have right := productOp.value with magma, magma2, ha, hb, unitIn, unitIn2245    rw xShape246    constructor247    . cc248    . cc249  have pInverse : Inverse(G.carrier × H.carrier, productOp(G.carrier, G.mul, H.carrier, H.mul), (G.one, H.one), productInv(G.carrier, G.inv, H.carrier, H.inv))250    have invGraph := productInv.function with invFunction, invFunction2251    unfold Inverse252    refine ⟨invGraph, ?_⟩253    intros X hX254    obtain ⟨boundX, a, ha, b, hb, xShape⟩ := product.membership.forward with hX255    have invA : a⁻¹ ∈ G by typecheck256    have invB : b⁻¹ ∈ H by typecheck257    have inverseValue := productInv.value with invFunction, invFunction2, ha, hb258    have leftA : a⁻¹ * a = G.one := Group.inv_mul with *259    have leftB : b⁻¹ * b = H.one := Group.inv_mul with *260    have rightA : a * a⁻¹ = G.one := Group.mul_inv with *261    have rightB : b * b⁻¹ = H.one := Group.mul_inv with *262    have left := productOp.value with magma, magma2, invA, invB, ha, hb263    have right := productOp.value with magma, magma2, ha, hb, invA, invB264    rw xShape265    constructor266    . cc267    . cc268  unfold productGroup269  apply Group.of_parts270  simp [IsGroup, IsMonoid, IsSemigroup]271272instance productGroup.pair_mem (a : G) (b : H)273  shows (a, b) ∈ Group.carrier(productGroup(G, H))274proof275  rw productGroup.carrierOf276  exact product.pair with *277278theorem productGroup.abelian279  requires abelian : AbelianGroup(G)280  requires abelian2 : AbelianGroup(H)281  shows AbelianGroup(productGroup(G, H))282proof283  have magma := IsGroup.magma with (Group.parts with group)284  have magma2 := IsGroup.magma with (Group.parts with group2)285  have pGroup := Group.parts with (productGroup.group with group, group2)286  have pCommutative : Commutative(G.carrier × H.carrier, productOp(G.carrier, G.mul, H.carrier, H.mul))287    intros X hX Y hY288    obtain ⟨boundX, a, ha, b, hb, xShape⟩ := product.membership.forward with hX289    obtain ⟨boundY, c, hc, d, hd, yShape⟩ := product.membership.forward with hY290    have xy := productOp.value with magma, magma2, ha, hb, hc, hd291    have yx := productOp.value with magma, magma2, hc, hd, ha, hb292    have swapA : a * c = c * a := mul_comm with *293    have swapB : b * d = d * b := mul_comm with *294    rw [xShape, yShape]295    cc296  rw [productGroup.carrierOf, productGroup.operation, productGroup.unit, productGroup.inverse] at pGroup297  unfold productGroup298  apply AbelianGroup.of_parts299  unfold IsAbelianGroup300  exact ⟨pGroup, pCommutative⟩301302-- The projections are surjective homomorphisms.303theorem firstProjection.hom304  shows firstProjection(G.carrier, H.carrier) : productGroup(G, H) →* G305proof306  have pGroup := productGroup.group with group, group2307  have function := firstProjection.function at G.carrier, H.carrier308  have function2 : firstProjection(G.carrier, H.carrier) : Group.carrier(productGroup(G, H)) → G.carrier309    rw productGroup.carrierOf310    exact function311  apply GroupHom.mk with pGroup, group, function2312  intros X hX Y hY313  rw productGroup.carrierOf at hX314  rw productGroup.carrierOf at hY315  obtain ⟨boundX, a, ha, b, hb, xShape⟩ := product.membership.forward with hX316  obtain ⟨boundY, c, hc, d, hd, yShape⟩ := product.membership.forward with hY317  have ac : a * c ∈ G by typecheck318  have bd : b * d ∈ H by typecheck319  have xy : Group.mul(productGroup(G, H))((a, b), (c, d)) = (a * c, b * d) := productGroup.mul with *320  have vx := firstProjection.pair with ha, hb321  have vy := firstProjection.pair with hc, hd322  have output := firstProjection.pair with ac, bd323  rw [xShape, yShape]324  cc325326theorem secondProjection.hom327  shows secondProjection(G.carrier, H.carrier) : productGroup(G, H) →* H328proof329  have pGroup := productGroup.group with group, group2330  have function := secondProjection.function at G.carrier, H.carrier331  have function2 : secondProjection(G.carrier, H.carrier) : Group.carrier(productGroup(G, H)) → H.carrier332    rw productGroup.carrierOf333    exact function334  apply GroupHom.mk with pGroup, group2, function2335  intros X hX Y hY336  rw productGroup.carrierOf at hX337  rw productGroup.carrierOf at hY338  obtain ⟨boundX, a, ha, b, hb, xShape⟩ := product.membership.forward with hX339  obtain ⟨boundY, c, hc, d, hd, yShape⟩ := product.membership.forward with hY340  have ac : a * c ∈ G by typecheck341  have bd : b * d ∈ H by typecheck342  have xy : Group.mul(productGroup(G, H))((a, b), (c, d)) = (a * c, b * d) := productGroup.mul with *343  have vx := secondProjection.pair with ha, hb344  have vy := secondProjection.pair with hc, hd345  have output := secondProjection.pair with ac, bd346  rw [xShape, yShape]347  cc348349theorem firstProjection.surjective350  shows SurjectiveBetween(firstProjection(G.carrier, H.carrier), Group.carrier(productGroup(G, H)), G.carrier)351proof352  have function := firstProjection.function at G.carrier, H.carrier353  have unitIn : H.one ∈ H := Group.one_mem with *354  rw productGroup.carrierOf355  constructor356  . exact function357  . intros a ha358    have pair := product.pair at a, H.one, G.carrier, H.carrier with *359    have value := firstProjection.pair with ha, unitIn360    have edge := FunctionBetween.relates_apply with function, pair361    refine ⟨(a, H.one), pair, ?_⟩362    rwa value at edge363364theorem secondProjection.surjective365  shows SurjectiveBetween(secondProjection(G.carrier, H.carrier), Group.carrier(productGroup(G, H)), H.carrier)366proof367  have function := secondProjection.function at G.carrier, H.carrier368  have unitIn : G.one ∈ G := Group.one_mem with *369  rw productGroup.carrierOf370  constructor371  . exact function372  . intros b hb373    have pair := product.pair at G.one, b, G.carrier, H.carrier with *374    have value := secondProjection.pair with unitIn, hb375    have edge := FunctionBetween.relates_apply with function, pair376    refine ⟨(G.one, b), pair, ?_⟩377    rwa value at edge378379-- The kernels of the projections are the two factors.380theorem firstProjection.kernel381  shows kernel(firstProjection(G.carrier, H.carrier), productGroup(G, H), G) = {G.one} × H.carrier382proof383  have unitIn : G.one ∈ G := Group.one_mem with *384  ext X385  constructor386  . intro hX387    obtain ⟨member, value⟩ := kernel.membership.forward with hX388    rw productGroup.carrierOf at member389    obtain ⟨bound, a, ha, b, hb, shape⟩ := product.membership.forward with member390    have projected := firstProjection.pair with ha, hb391    have aUnit : a = G.one by cc392    have inUnit : a ∈ {G.one}393      rw aUnit394      exact singleton.self395    rw shape396    exact product.pair with inUnit, hb397  . intro hX398    obtain ⟨bound, a, ha, b, hb, shape⟩ := product.membership.forward with hX399    have aUnit := singleton.membership.forward with ha400    have aIn : a ∈ G by rwa aUnit401    have member := product.pair at a, b, G.carrier, H.carrier with *402    have projected := firstProjection.pair with aIn, hb403    have vanishes : firstProjection(G.carrier, H.carrier)(X) = G.one by cc404    have memberX : X ∈ Group.carrier(productGroup(G, H))405      rw productGroup.carrierOf406      rwa shape407    exact kernel.of_value with memberX, vanishes408409theorem secondProjection.kernel410  shows kernel(secondProjection(G.carrier, H.carrier), productGroup(G, H), H) = G.carrier × {H.one}411proof412  have unitIn : H.one ∈ H := Group.one_mem with *413  ext X414  constructor415  . intro hX416    obtain ⟨member, value⟩ := kernel.membership.forward with hX417    rw productGroup.carrierOf at member418    obtain ⟨bound, a, ha, b, hb, shape⟩ := product.membership.forward with member419    have projected := secondProjection.pair with ha, hb420    have bUnit : b = H.one by cc421    have inUnit : b ∈ {H.one}422      rw bUnit423      exact singleton.self424    rw shape425    exact product.pair with ha, inUnit426  . intro hX427    obtain ⟨bound, a, ha, b, hb, shape⟩ := product.membership.forward with hX428    have bUnit := singleton.membership.forward with hb429    have bIn : b ∈ H by rwa bUnit430    have member := product.pair at a, b, G.carrier, H.carrier with *431    have projected := secondProjection.pair with ha, bIn432    have vanishes : secondProjection(G.carrier, H.carrier)(X) = H.one by cc433    have memberX : X ∈ Group.carrier(productGroup(G, H))434      rw productGroup.carrierOf435      rwa shape436    exact kernel.of_value with memberX, vanishes437438-- Each factor is a normal subgroup of the product.439theorem productGroup.right_factor_normal440  shows NormalSubgroup({G.one} × H.carrier, productGroup(G, H))441proof442  have hom := firstProjection.hom with group, group2443  have normal := GroupHom.kernel_normal with hom444  have same := firstProjection.kernel with group, group2445  rwa same at normal446447theorem productGroup.left_factor_normal448  shows NormalSubgroup(G.carrier × {H.one}, productGroup(G, H))449proof450  have hom := secondProjection.hom with group, group2451  have normal := GroupHom.kernel_normal with hom452  have same := secondProjection.kernel with group, group2453  rwa same at normal454455end ProductGroup456457-- The embedding of the left factor.458def leftEmbedding (A B unit2 : Set) : Set :=459  { q ∈ A × (A × B) | ∃ a ∈ A, q = (a ↦ (a, unit2)) }460461theorem leftEmbedding.relates (A B unit2 a : Set)462  requires unitIn : unit2 ∈ B463  requires ha : a ∈ A464  shows relates(leftEmbedding(A, B, unit2), a, (a, unit2))465proof466  have pair := product.pair at a, unit2, A, B with *467  have bounded := product.pair at a, (a, unit2), A, A × B with *468  unfold relates469  apply leftEmbedding.membership.backward470  refine ⟨bounded, a, ha, rfl⟩471472theorem leftEmbedding.function (A B unit2 : Set)473  requires unitIn : unit2 ∈ B474  shows leftEmbedding(A, B, unit2) : A → A × B475proof476  unfold FunctionBetween477  refine ⟨?_, ?_, ?_⟩478  . intros q hq479    have parts := leftEmbedding.membership.forward with hq480    exact parts.left481  . intros p y edge z edge2482    unfold relates at edge483    unfold relates at edge2484    obtain ⟨bounded, a, ha, shape⟩ := leftEmbedding.membership.forward with edge485    obtain ⟨bounded2, a2, ha2, shape2⟩ := leftEmbedding.membership.forward with edge2486    have outer := orderedPair.injective with shape487    have outer2 := orderedPair.injective with shape2488    cc489  . intros a ha490    have pair := product.pair at a, unit2, A, B with *491    have edge := leftEmbedding.relates with unitIn, ha492    exact ⟨(a, unit2), pair, edge⟩493494theorem leftEmbedding.value (A B unit2 a : Set)495  requires unitIn : unit2 ∈ B496  requires ha : a ∈ A497  shows leftEmbedding(A, B, unit2)(a) = (a, unit2)498proof499  have function := leftEmbedding.function at A, B, unit2 with unitIn500  have edge := leftEmbedding.relates with unitIn, ha501  exact FunctionBetween.apply_value with function, ha, edge502503theorem leftEmbedding.injective (A B unit2 : Set)504  requires unitIn : unit2 ∈ B505  shows InjectiveBetween(leftEmbedding(A, B, unit2), A, A × B)506proof507  have function := leftEmbedding.function at A, B, unit2 with unitIn508  constructor509  . exact function510  . intros x hx y hy z hz hxz hyz511    have vx := FunctionBetween.apply_value with function, hx, hxz512    have vy := FunctionBetween.apply_value with function, hy, hyz513    have ex := leftEmbedding.value with unitIn, hx514    have ey := leftEmbedding.value with unitIn, hy515    have pairs : (x, unit2) = (y, unit2) by cc516    have coordinates := orderedPair.injective with pairs517    exact coordinates.left518519theorem leftEmbedding.first_projection (A B unit2 a : Set)520  requires unitIn : unit2 ∈ B521  requires ha : a ∈ A522  shows firstProjection(A, B)(leftEmbedding(A, B, unit2)(a)) = a523proof524  have value := leftEmbedding.value with unitIn, ha525  have projected := firstProjection.pair with ha, unitIn526  rw value527  exact projected528529section Embedding530variable (G H : Set)531hypothesis group : Group(G)532hypothesis group2 : Group(H)533534theorem leftEmbedding.hom535  shows leftEmbedding(G.carrier, H.carrier, H.one) : G →* productGroup(G, H)536proof537  have pGroup := productGroup.group with group, group2538  have unitIn : H.one ∈ H := Group.one_mem with *539  have function := leftEmbedding.function at G.carrier, H.carrier, H.one with unitIn540  have function2 : leftEmbedding(G.carrier, H.carrier, H.one) : G.carrier → Group.carrier(productGroup(G, H))541    rw productGroup.carrierOf542    exact function543  apply GroupHom.mk with group, pGroup, function2544  intros x hx y hy545  have closed : x * y ∈ G by typecheck546  have vx := leftEmbedding.value with unitIn, hx547  have vy := leftEmbedding.value with unitIn, hy548  have output := leftEmbedding.value with unitIn, closed549  have combined : Group.mul(productGroup(G, H))((x, H.one), (y, H.one)) = (x * y, H.one * H.one) :=550    productGroup.mul with *551  have identity : H.one * H.one = H.one := one_mul with *552  cc553554end Embedding555