-- Left and right cosets of a subgroup: each coset is generated by any of
-- its members, two cosets that share a point coincide, membership through
-- the difference of representatives, and the set of all left cosets
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Group.Coset
import Subgroup

-- The left coset g * H and the right coset H * g of a subset H of G.
def leftCoset (G g H : Set) : Set := { y ∈ G.carrier | ∃ h ∈ H, y = G.mul(g, h) }
def rightCoset (G g H : Set) : Set := { y ∈ G.carrier | ∃ h ∈ H, y = G.mul(h, g) }

-- The set of all left cosets of H.
def leftCosets (G H : Set) : Set :=
  { C ∈ 𝒫(G.carrier) | ∃ g ∈ G.carrier, C = leftCoset(G, g, H) }

-- The left coset leftCoset(G, g, H) is written g • H wherever a hypothesis
-- in scope supplies the group.
notation infixr 73 "•" => leftCoset(G, _, _) via hypothesis Group(G) for G.carrier
notation infixr 73 "•" => leftCoset(G, _, _) via hypothesis Subgroup(H, G) for G.carrier

theorem leftCoset.subset (G g H : Set)
  shows leftCoset(G, g, H) ⊆ G.carrier
proof
  intros y hy
  have parts := leftCoset.membership.forward with hy
  exact parts.left

theorem rightCoset.subset (G g H : Set)
  shows rightCoset(G, g, H) ⊆ G.carrier
proof
  intros y hy
  have parts := rightCoset.membership.forward with hy
  exact parts.left

theorem leftCosets.subset_powerset (G H : Set)
  shows leftCosets(G, H) ⊆ 𝒫(G.carrier)
proof
  intros C hC
  have parts := leftCosets.membership.forward with hC
  exact parts.left

theorem leftCosets.coset_member (G H g : Set)
  requires hg : g ∈ G.carrier
  shows leftCoset(G, g, H) ∈ leftCosets(G, H)
proof
  have subset := leftCoset.subset at G, g, H
  have bounded := powerset.membership_iff.backward with subset
  exact leftCosets.membership.backward with ⟨bounded, g, hg, rfl⟩

section Cosets
variable (G H : Set)
hypothesis group : Group(G)
hypothesis subgroup : Subgroup(H, G)

theorem leftCoset.mul_mem (g : G) (h : H)
  shows g * h ∈ g • H
proof
  have product : g * h ∈ G by typecheck
  have hIn : h ∈ H by assumption
  exact leftCoset.membership.backward with ⟨product, h, hIn, rfl⟩

theorem rightCoset.mul_mem (g : G) (h : H)
  shows h * g ∈ rightCoset(G, g, H)
proof
  have product : h * g ∈ G by typecheck
  have hIn : h ∈ H by assumption
  exact rightCoset.membership.backward with ⟨product, h, hIn, rfl⟩

theorem leftCoset.self (g : G)
  shows g ∈ g • H
proof
  have product : g * G.one ∈ g • H := leftCoset.mul_mem with *
  rwa mul_one at product

theorem rightCoset.self (g : G)
  shows g ∈ rightCoset(G, g, H)
proof
  have product : G.one * g ∈ rightCoset(G, g, H) := rightCoset.mul_mem with *
  rwa one_mul at product

-- Membership in a coset through the difference of representatives.
theorem leftCoset.mem_iff (x y : G)
  shows y ∈ x • H ↔ x⁻¹ * y ∈ H
proof
  constructor
  . intro member
    obtain ⟨yIn, h, hH, yEq⟩ := leftCoset.membership.forward with member
    rw [yEq, inv_mul_cancel_left]
    exact hH
  . intro member
    have cancel : x * (x⁻¹ * y) = y := mul_inv_cancel_left with *
    have yIn : y ∈ G by assumption
    apply leftCoset.membership.backward
    refine ⟨yIn, x⁻¹ * y, member, ?_⟩
    symm
    exact cancel

theorem rightCoset.mem_iff (x y : G)
  shows y ∈ rightCoset(G, x, H) ↔ y * x⁻¹ ∈ H
proof
  constructor
  . intro member
    obtain ⟨yIn, h, hH, yEq⟩ := rightCoset.membership.forward with member
    rw [yEq, mul_inv_cancel_right]
    exact hH
  . intro member
    have cancel : y * x⁻¹ * x = y := inv_mul_cancel_right with *
    have yIn : y ∈ G by assumption
    apply rightCoset.membership.backward
    refine ⟨yIn, y * x⁻¹, member, ?_⟩
    symm
    exact cancel

-- Any member of a coset generates it.
theorem leftCoset.of_member (g : G) (y : Set)
  requires hy : y ∈ g • H
  shows y • H = g • H
proof
  obtain ⟨yIn, h0, h0In, yEq⟩ := leftCoset.membership.forward with hy
  ext z
  constructor
  . intro hz
    obtain ⟨zIn, h, hH, zEq⟩ := leftCoset.membership.forward with hz
    have product : h0 * h ∈ H := Subgroup.mul_mem with *
    apply leftCoset.membership.backward
    refine ⟨zIn, h0 * h, product, ?_⟩
    rw [zEq, yEq, mul_assoc]
    rfl
  . intro hz
    obtain ⟨zIn, h, hH, zEq⟩ := leftCoset.membership.forward with hz
    have product : h0⁻¹ * h ∈ H := Subgroup.mul_mem with *
    apply leftCoset.membership.backward
    refine ⟨zIn, h0⁻¹ * h, product, ?_⟩
    rw [zEq, yEq, mul_assoc, mul_inv_cancel_left]
    rfl

theorem leftCoset.eq_of_common (g k : G) (z : Set)
  requires hz : z ∈ g • H
  requires hz2 : z ∈ k • H
  shows g • H = k • H
proof
  have first : z • H = g • H := leftCoset.of_member with *
  have second : z • H = k • H := leftCoset.of_member with *
  rwa first at second

theorem leftCoset.eq_iff (x y : G)
  shows x • H = y • H ↔ x⁻¹ * y ∈ H
proof
  have criterion : y ∈ x • H ↔ x⁻¹ * y ∈ H := leftCoset.mem_iff with *
  have selfY : y ∈ y • H := leftCoset.self with *
  constructor
  . intro equal
    have member : y ∈ x • H by rwa equal
    exact criterion.forward with member
  . intro member
    have inside := criterion.backward with member
    have equal : y • H = x • H := leftCoset.of_member with *
    symm
    exact equal

theorem leftCoset.one
  shows G.one • H = H
proof
  ext y
  constructor
  . intro hy
    obtain ⟨yIn, h, hH, yEq⟩ := leftCoset.membership.forward with hy
    rw [yEq, one_mul]
    exact hH
  . intro hy
    have yIn : y ∈ G := Subgroup.mem_carrier with *
    have identity : G.one * y = y := one_mul with *
    apply leftCoset.membership.backward
    refine ⟨yIn, y, hy, ?_⟩
    symm
    exact identity

theorem leftCoset.eq_self_iff (x : G)
  shows x • H = H ↔ x ∈ H
proof
  have criterion : x • H = G.one • H ↔ x⁻¹ * G.one ∈ H :=
    leftCoset.eq_iff with *
  have inverseCriterion : x⁻¹ ∈ H ↔ x ∈ H := Subgroup.inv_mem_iff with *
  rw [leftCoset.one, mul_one] at criterion
  constructor
  . intro equal
    have member := criterion.forward with equal
    exact inverseCriterion.forward with member
  . intro member
    have inverse := inverseCriterion.backward with member
    exact criterion.backward with inverse

theorem leftCosets.representative (C : Set)
  requires hC : C ∈ leftCosets(G, H)
  shows ∃ g ∈ G, g ∈ C
proof
  obtain ⟨bound, g, hg, same⟩ := leftCosets.membership.forward with hC
  have self : g ∈ g • H := leftCoset.self with *
  witness g
  constructor
  . exact hg
  . rw same
    exact self

end Cosets