How do I express the Subgroup Criterion?

Stream: new members

[Khang]

Subgroup Criterion as in the 1st proposition of Dummit and Foote's Abstract Algebra.

I'm relatively new to Lean, and what I have so far is individual proofs in both directions, but they don't quite gel together in an iff statement. Is there an idiomatic way of writing out the iff statement? That would be of great help, thanks.

import Mathlib.Algebra.Group.Subgroup.Basic

universe u

variable {G : Type u} [Group G]

Forward direction:

example (H : Set G) (h₀ : H.Nonempty) (h : ∀ x y : G, x ∈ H → y ∈ H → x * y⁻¹ ∈ H) :
  Subgroup G := by
  have one_mem' : 1 ∈ H := let ⟨x, hx⟩ := h₀; mul_inv_cancel x ▸ h x x hx hx
  have inv_mem' {x : G} : x ∈ H → x⁻¹ ∈ H := fun hx => one_mul x⁻¹ ▸ h 1 x one_mem' hx
  have mul_mem' {x y : G} : x ∈ H → y ∈ H → x * y ∈ H := fun hx hy => inv_inv y ▸ h x y⁻¹ hx (inv_mem' hy)
  exact { carrier := H, mul_mem' := mul_mem', one_mem' := one_mem', inv_mem' := inv_mem' }

Backward direction(s)

example (H : Subgroup G) : Nonempty H ∧ (∀ x y, x ∈ H → y ∈ H → x * y⁻¹ ∈ H) :=
  ⟨One.instNonempty, fun x y hx hy => H.mul_mem' hx (H.inv_mem' hy)⟩

example (H : Subgroup G) : (H : Set G).Nonempty ∧ (∀ x y, x ∈ H → y ∈ H → x * y⁻¹ ∈ H) :=
  ⟨H.coe_nonempty, fun x y hx hy => H.mul_mem' hx (H.inv_mem' hy)⟩

[Kenny Lau]

@Khang the iff statement is mathematically neat and all, but is not helpful for lean

[Kenny Lau]

import Mathlib.Algebra.Group.Subgroup.Basic

universe u

variable {G : Type u} [Group G]

theorem exists_subgroup_iff (H : Set G) :
    (∃ s : Subgroup G, s = H) ↔ H.Nonempty ∧ ∀ x y : G, x ∈ H → y ∈ H → x * y⁻¹ ∈ H :=
  sorry

[Kenny Lau]

import Mathlib.Algebra.Group.Subgroup.Basic

universe u

variable {G : Type u} [Group G]

def Subgroup.ofCondition
    (H : Set G) (h₀ : H.Nonempty) (h : ∀ x y : G, x ∈ H → y ∈ H → x * y⁻¹ ∈ H) :
    Subgroup G :=
  have one_mem' : 1 ∈ H :=
    let ⟨x, hx⟩ := h₀; mul_inv_cancel x ▸ h x x hx hx
  have inv_mem' {x : G} (hx : x ∈ H) : x⁻¹ ∈ H :=
    one_mul x⁻¹ ▸ h 1 x one_mem' hx
  have mul_mem' {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x * y ∈ H :=
    inv_inv y ▸ h x y⁻¹ hx (inv_mem' hy)
  { carrier := H,
    mul_mem' := mul_mem'
    one_mem' := one_mem'
    inv_mem' := inv_mem' }

theorem Subgroup.condition (H : Subgroup G) :
    (H : Set G).Nonempty ∧ (∀ x y, x ∈ H → y ∈ H → x * y⁻¹ ∈ H) :=
  ⟨H.coe_nonempty, fun _ _ hx hy => H.mul_mem' hx (H.inv_mem' hy)⟩

theorem exists_subgroup_iff (H : Set G) :
    (∃ s : Subgroup G, s = H) ↔ H.Nonempty ∧ ∀ x y : G, x ∈ H → y ∈ H → x * y⁻¹ ∈ H :=
  ⟨fun ⟨s, hs⟩ ↦ hs ▸ s.condition,
  fun h ↦ ⟨.ofCondition H h.left h.right, rfl⟩⟩

[Khang]

Kenny Lau said:

Khang the iff statement is mathematically neat and all, but is not helpful for lean

I see. I guess the iff statement might end up being unwieldly. Thanks for the suggestion!