Grace/Cumulus/Algebra/Group/CosetSplit.g17

Open in Workbench Download source

Imports

Lagrange · Set.Choice

Declarations

Source

1-- A chosen representative of each left coset, and the bijection2-- g ↦ (gH, rep(gH)⁻¹ * g) from a group onto the product of the coset space3-- and the subgroup, with no finiteness assumed; this is the one place in4-- group theory up to Lagrange's theorem that selects with Choice5-- 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.CosetSplit11import Lagrange12import Set.Choice1314-- A chosen representative of each coset.15defchoose cosetRepresentative (G H C : Set) (r ∈ G.carrier) := r ∈ C16requires group : Group(G)17requires subgroup : Subgroup(H, G)18requires hC : C ∈ leftCosets(G, H)19proof20  exact leftCosets.representative with group, subgroup, hC2122-- Each element g is sent to its coset and to its position rep(gH)⁻¹ * g23-- in H.24defgraph cosetSplit (G H : Set) (g ∈ G.carrier) : leftCosets(G, H) × H :=25  (g • H, cosetRepresentative(G, H, g • H)⁻¹ * g)26requires group : Group(G)27requires subgroup : Subgroup(H, G)28proof29  have cosetIn := leftCosets.coset_member at G, H, g with member30  have selected := cosetRepresentative.selected at G, H, g • H with group, subgroup, cosetIn31  have repIn := selected.left32  obtain ⟨repBound, h0, h0In, repEq⟩ := leftCoset.membership.forward with selected.right33  have position : cosetRepresentative(G, H, g • H)⁻¹ * g = h0⁻¹34    rw [repEq, mul_inv_rev, inv_mul_cancel_right]35    rfl36  apply product.pair_membership.backward37  constructor38  . exact cosetIn39  . rw position40    exact Subgroup.inv_mem with *4142section CosetSplit43variable (G H : Set)44hypothesis group : Group(G)45hypothesis subgroup : Subgroup(H, G)4647-- The split g ↦ (gH, rep(gH)⁻¹ * g) is a bijection onto the product of the48-- coset space and the subgroup, with no finiteness assumed.49theorem cosetSplit.injective50  shows InjectiveBetween(cosetSplit(G, H), G.carrier, leftCosets(G, H) × H)51proof52  have function := cosetSplit.function at G, H with *53  constructor54  . exact function55  . intros x hx y hy z hz hxz hyz56    have xValue := FunctionBetween.apply_value with function, hx, hxz57    have yValue := FunctionBetween.apply_value with function, hy, hyz58    have xPair := cosetSplit.value at G, H, x with *59    have yPair := cosetSplit.value at G, H, y with *60    rw xValue at xPair61    rw [yValue, xPair] at yPair62    have components := orderedPair.injective with yPair63    have samePosition := components.right64    rw components.left at samePosition65    have cosetIn := leftCosets.coset_member at G, H, y with hy66    have selected := cosetRepresentative.selected with group, subgroup, cosetIn67    have repIn := selected.left68    exact mul_left_cancel with *6970theorem cosetSplit.surjective71  shows SurjectiveBetween(cosetSplit(G, H), G.carrier, leftCosets(G, H) × H)72proof73  have function := cosetSplit.function at G, H with *74  constructor75  . exact function76  . intros p hp77    obtain ⟨bound, C, hC, h, hh, pEq⟩ := product.membership.forward with hp78    have selected := cosetRepresentative.selected with group, subgroup, hC79    have repIn := selected.left80    have repC := selected.right81    obtain ⟨cosetBound, g0, hg0, CEq⟩ := leftCosets.membership.forward with hC82    have gIn : cosetRepresentative(G, H, C) * h ∈ G by typecheck83    witness cosetRepresentative(G, H, C) * h84    constructor85    . exact gIn86    . have value := cosetSplit.value at G, H, cosetRepresentative(G, H, C) * h with *87      have gCoset : (cosetRepresentative(G, H, C) * h) • H = C88        symm at CEq89        have repIn2 : cosetRepresentative(G, H, C) ∈ g0 • H by rwa CEq90        have repCoset : cosetRepresentative(G, H, C) • H = g0 • H :=91          leftCoset.of_member with *92        have gIn2 : cosetRepresentative(G, H, C) * h ∈ cosetRepresentative(G, H, C) • H :=93          leftCoset.mul_mem with *94        have gCoset0 : (cosetRepresentative(G, H, C) * h) • H =95            cosetRepresentative(G, H, C) • H := leftCoset.of_member with *96        rw [gCoset0, repCoset, CEq]97        rfl98      have position : cosetRepresentative(G, H, C)⁻¹ * (cosetRepresentative(G, H, C) * h) = h :=99        inv_mul_cancel_left with *100      rw [gCoset, position] at value101      have related := FunctionBetween.relates_apply with function, gIn102      rw value at related103      rwa pEq104105theorem cosetSplit.bijective106  shows BijectiveBetween(cosetSplit(G, H), G.carrier, leftCosets(G, H) × H)107proof108  constructor109  . exact cosetSplit.injective with group, subgroup110  . exact cosetSplit.surjective with group, subgroup111112theorem Group.equipotent_cosets_product113  shows G.carrier ≃ leftCosets(G, H) × H114proof115  witness cosetSplit(G, H)116  exact cosetSplit.bijective with group, subgroup117end CosetSplit118