case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ normalCore H ≤ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))

case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H)) ≤ normalCore H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ normalCore H = MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
apply le_antisymm
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
⊢ g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ normalCore H ≤ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
intro g hg
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
⊢ ∀ (x : G ⧸ H), ↑(↑(MulAction.toPermHom G (G ⧸ H)) g) x = ↑1 x
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
⊢ g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
apply Equiv.Perm.ext
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
⊢ ∀ (z : G), ↑(↑(MulAction.toPermHom G (G ⧸ H)) g) ↑z = ↑1 ↑z
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
⊢ ∀ (x : G ⧸ H), ↑(↑(MulAction.toPermHom G (G ⧸ H)) g) x = ↑1 x
refine' fun q ↦ QuotientGroup.induction_on q _
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
g' : G
⊢ (g • g')⁻¹ * g' ∈ H
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
⊢ ∀ (z : G), ↑(↑(MulAction.toPermHom G (G ⧸ H)) g) ↑z = ↑1 ↑z
refine' fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr _)
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
g' : G
⊢ (g • g')⁻¹ * g' ∈ H
rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]
no goals
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H
exact H.normalCore.inv_mem hg g'⁻¹
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
⊢ g ∈ H
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H)) ≤ normalCore H
refine' (Subgroup.normal_le_normalCore.mpr fun g hg => _)
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
⊢ ↑(g * 1) = ↑1
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
⊢ g ∈ H
rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
no goals
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
⊢ ↑(g * 1) = ↑1
exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))