induction lemmas for semidirect product

Stream: Is there code for X?

[Edward van de Meent]

i have defined a GroupHom using SemidirectProduct.lift, and i'd like to prove that it is injective by using the fact that the maps i used to define it are injective, and that the only overlap in the codomain is 1. I had guessed that to do this i could use some kind of closure-induction argument for the semidirect product, but i found none...
a first thing that would help is the following lemma:

import Mathlib.GroupTheory.SemidirectProduct

variable {N G : Type*} [Group N] [Group G] (hom : G →* MulAut N)
lemma SemidirectProduct.is_closure :
  Subgroup.closure ((Set.range SemidirectProduct.inl : Set (N ⋊[hom] G)) ∪ (Set.range SemidirectProduct.inr : Set (N ⋊[hom] G))) = ⊤ := sorry

ultimately, my goal is this:

variable {H:Type*} [Group H] (f₁ : N →* H) (f₂ : G →* H)
  (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁))
lemma SemidirectProduct.lift_inj (hf₁ : Function.Injective f₁) (hf2 : Function.Injective f₂)
    (hindep : f₁.range ⊓ f₂.range = ⊥)
    :
    Function.Injective (SemidirectProduct.lift f₁ f₂ h ) := sorry

[Edward van de Meent]

solution to second part

lemma SemidirectProduct.lift_inj (hf₁ : Function.Injective f₁) (hf₂ : Function.Injective f₂)
    (hindep : f₁.range ⊓ f₂.range = ⊥):
    Function.Injective (SemidirectProduct.lift f₁ f₂ h) := by
  rw [← MonoidHom.ker_eq_bot_iff, eq_bot_iff]
  intro x
  simp only [Subgroup.mem_bot]
  rw [MonoidHom.mem_ker]
  obtain ⟨x₁,x₂⟩ := x
  simp only [mk_eq_inl_mul_inr, map_mul, lift_inl, lift_inr]
  intro hinv
  obtain hinv' : f₁ x₁ = (f₂ x₂)⁻¹ := by
    rw [← one_mul (f₂ x₂)⁻¹]
    rw [← hinv]
    simp only [mul_inv_cancel_right]
  have him₁ : f₁ x₁ ∈ f₁.range := by simp only [MonoidHom.mem_range,
    exists_apply_eq_apply]
  have him₂ : f₁ x₁ ∈ f₂.range := by rw [hinv']; simp only [inv_mem_iff,
    MonoidHom.mem_range, exists_apply_eq_apply]
  have hone : f₁ x₁ ∈ ⊥ := by
    rw [← hindep]
    exact And.intro him₁ him₂
  simp only [Subgroup.mem_bot] at hone
  have hker : x₁ ∈ f₁.ker := by
    rw [MonoidHom.mem_ker f₁]
    exact hone

  rw [← MonoidHom.ker_eq_bot_iff] at hf₁ hf₂
  rw [hf₁] at hker
  simp only [Subgroup.mem_bot] at hker
  rw [hker] at hinv' ⊢
  simp only [map_one, one_eq_inv] at hinv'
  rw [← MonoidHom.mem_ker] at hinv'
  rw [hf₂] at hinv'
  simp only [Subgroup.mem_bot] at hinv'
  rw [hinv']
  simp only [map_one, mul_one]

[Kevin Buzzard]

I would prove the stronger theorem that every element of a semidirect product is equal to a product g*n. A general element of a Subgroup.closure is a random finite product so the stronger theorem looks easier to prove. You can then just use the fact that injective iff trivial kernel

[Edward van de Meent]

so you suggest using something like this?

lemma SemidirectProduct.factor (x : N ⋊[φ] G) :
    ∃ n g, x = SemidirectProduct.inl n * SemidirectProduct.inr g := by
  obtain ⟨n,g⟩ := x
  simp only [mk_eq_inl_mul_inr]
  use n,g

[Edward van de Meent]

my point is mostly that proving this closure property opens up the use of Subgroup.induction and variants

[Edward van de Meent]

which i imagine wouldn't be harmful

[Kevin Buzzard]

Sure, but now proving the closure property is easy

[Edward van de Meent]

ah, i see

[Kevin Buzzard]

(hopefully!)

[Kevin Buzzard]

I guess you just need to prove that the product of two things in S is in closure S, which could be a lemma in its own right

[Edward van de Meent]

it already is (sort of): docs#Subgroup.mul_mem_sup

[Edward van de Meent]

at least, the form i need

[Eric Wieser]

Edward van de Meent said:

so you suggest using something like this?

lemma SemidirectProduct.factor (x : N ⋊[φ] G) :
    ∃ n g, x = SemidirectProduct.inl n * SemidirectProduct.inr g := by
  obtain ⟨n,g⟩ := x
  simp only [mk_eq_inl_mul_inr]
  use n,g

This should be phrased as an induction principle

[Edward van de Meent]

protected lemma SemidirectProduct.induction {motive : N ⋊[φ] G → Prop} (x : N ⋊[φ] G)
    (left : ∀ n, motive (inl n))
    (right : ∀ g, motive (inr g))
    (mul : ∀ (n : N) (g : G), motive (inl n) → motive (inr g) → motive (inl n * inr g)) :
    motive x := by
  obtain ⟨x₁,x₂⟩ := x
  simp only [mk_eq_inl_mul_inr]
  exact mul _ _ (left x₁) (right x₂)

you mean like this?

[Edward van de Meent]

or like this:

protected lemma SemidirectProduct.induction' {motive : N ⋊[φ] G → Prop} (x : N ⋊[φ] G)
    (mul : ∀ (n : N) (g : G),motive (inl n * inr g)) :
    motive x := by
  obtain ⟨x₁,x₂⟩ := x
  simp only [mk_eq_inl_mul_inr]
  exact mul x₁ x₂

[Eric Wieser]

I meant the second one

[Eric Wieser]

But with @[elab_as_elim]