Theorem: OnCycleFactors.odd_of_mem_kerφ (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ ∀ i ∈ Equiv.Perm.cycleType g, Odd i
Tactic:
intro i hi
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ Odd i

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ Odd i
Tactic:
rw [Equiv.Perm.cycleType_def g, Multiset.mem_map] at hi
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
i : ℕ
hi : ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = i
⊢ Odd i

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
i : ℕ
hi : ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = i
⊢ Odd i
Tactic:
obtain ⟨c, hc, rfl⟩ := hi
State after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)

State before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)
Tactic:
rw [← Finset.mem_def] at hc
State after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)

State before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.sign c = 1
Tactic:
suffices c = θ g ⟨1, Pi.mulSingle ⟨c, hc⟩ ⟨c, Subgroup.mem_zpowers c⟩⟩ by
  rw [this]
  apply h
  change ConjAct.toConjAct _ ∈ _
  apply Subgroup.map_subtype_le
  rw [OnCycleFactors.hφ_ker_eq_θ_range]
  exact Set.mem_range_self _
State after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
⊢ c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })

State before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
⊢ c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
Tactic:
rw [θ_apply_single]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : Equiv.Perm.sign c = 1
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)
Tactic:
rw [Equiv.Perm.IsCycle.sign _, neg_eq_iff_eq_neg] at this
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : Equiv.Perm.sign c = 1
⊢ Equiv.Perm.IsCycle c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)
Tactic:
rw [Nat.odd_iff_not_even, Function.comp_apply]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ ¬Even (Equiv.Perm.support c).card

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ ¬Even (Equiv.Perm.support c).card
Tactic:
rw [← neg_one_pow_eq_one_iff_even (R := ℤˣ) (by norm_num), this, ← Units.eq_iff]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ ¬↑(-1) = ↑1

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ ¬↑(-1) = ↑1
Tactic:
norm_num
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ -1 ≠ 1
Tactic:
norm_num
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : Equiv.Perm.sign c = 1
⊢ Equiv.Perm.IsCycle c
Tactic:
rw [Equiv.Perm.mem_cycleFactorsFinset_iff] at hc
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : Equiv.Perm.IsCycle c ∧ ∀ a ∈ Equiv.Perm.support c, c a = g a
this : Equiv.Perm.sign c = 1
⊢ Equiv.Perm.IsCycle c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : Equiv.Perm.IsCycle c ∧ ∀ a ∈ Equiv.Perm.support c, c a = g a
this : Equiv.Perm.sign c = 1
⊢ Equiv.Perm.IsCycle c
Tactic:
exact hc.left
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Equiv.Perm.sign c = 1
Tactic:
rw [this]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Equiv.Perm.sign ((θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })) = 1

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Equiv.Perm.sign ((θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })) = 1
Tactic:
apply h
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }) ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }) ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
change ConjAct.toConjAct _ ∈ _
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ ConjAct.toConjAct
      {
        toFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
        invFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
        left_inv := ⋯, right_inv := ⋯ } ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ ConjAct.toConjAct
      {
        toFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
        invFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
        left_inv := ⋯, right_inv := ⋯ } ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
apply Subgroup.map_subtype_le
State after:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ ConjAct.toConjAct
      {
        toFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
        invFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
        left_inv := ⋯, right_inv := ⋯ } ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ?a.K✝

case a.K
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Subgroup ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)

State before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ ConjAct.toConjAct
      {
        toFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
        invFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
        left_inv := ⋯, right_inv := ⋯ } ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ?a.K✝

case a.K
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Subgroup ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
Tactic:
rw [OnCycleFactors.hφ_ker_eq_θ_range]
State after:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ {
      toFun :=
        θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
          (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
      invFun :=
        θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
          (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
      left_inv := ⋯, right_inv := ⋯ } ∈
    Set.range ⇑(θ g)

State before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ {
      toFun :=
        θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
          (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
      invFun :=
        θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
          (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
      left_inv := ⋯, right_inv := ⋯ } ∈
    Set.range ⇑(θ g)
Tactic:
exact Set.mem_range_self _
State after:
no goals