FLT/Slop/PGL2/FiniteSubgroups/PSLRecognition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Recognising PSL₂(𝔽_q) inside PGL₂(𝔽̄_p)

Let G be a finite subgroup of PGLOf (K p) = PGL₂(𝔽̄_p) of order (q² - 1) * q / 2 (q = p^m) arising in the wild case of Dickson's classification. This file shows that after conjugation G lies in the image of PGL₂(𝔽_q) → PGL₂(𝔽̄_p) (Dickson.psl_G_le_pgl_range_from_orbit), the key step in identifying G with PSL₂(𝔽_q).

The argument runs through:

Imports (1)
Imported by 2 files
  1. theorem Dickson.sum_of_two_squares_Fq line 51 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, GE.ge, HPow.hPow, Dickson.K, Membership.mem, Set, Dickson.FqInK, Exists, And, Eq, HAdd.hAdd, ZMod

    Proof uses: Fintype.card, GaloisField, Dickson.instFintypeGaloisField, Eq.mpr, Nat.card, id, congrArg, Fintype.card_eq_nat_card, GaloisField.card, Eq.refl, RingHom, Dickson.galoisFieldRingHom, Multiset, Polynomial, Polynomial.map, Algebra.algebraMap, HSub.hSub, Polynomial.X, HMul.hMul, Polynomial.C and 105 more

    134 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

    Open to load the checked before-and-after goal states.

  2. theorem Dickson.sq_is_half_root_or_zero line 94 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.K, Membership.mem, Set, Dickson.FqInK, Or, Eq, HPow.hPow, ZMod, And, Ne, HDiv.hDiv, HSub.hSub

    Proof uses: id, eq_or_ne, Or.inl, zero_pow, two_ne_zero, Eq.symm, Or.inr, And.intro, pow_ne_zero, Dvd.dvd, Eq.mpr, Even, congrArg, propext, even_iff_two_dvd, Iff, Nat.even_sub, Nat.one_le_pow, Nat.Prime.pos, Fact.out and 26 more

    92 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

    Open to load the checked before-and-after goal states.

  3. theorem Dickson.additive_subgroup_eq_F_q_from_squares line 112 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, GE.ge, HPow.hPow, Set, Dickson.K, Eq, Set.ncard, Membership.mem, HAdd.hAdd, ZMod, HDiv.hDiv, HSub.hSub, Ne, HMul.hMul, Dickson.FqInK

    Proof uses: Or, And, Dickson.sq_is_half_root_or_zero, Eq.rec, Eq.symm, mul_one, LE.le, Exists, Dickson.sum_of_two_squares_Fq, Set.eq_of_subset_of_ncard_le, Eq.mpr, id, congrArg, Dickson.F_q_card, le_refl, Set.finite_of_ncard_pos, LT.lt, pow_pos, Nat.Prime.pos, Fact.out

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  4. theorem Dickson.sylow_order_of_psl_order line 135 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, Eq, Nat.card, HDiv.hDiv and 4 more

    Proof uses: Dvd.dvd, Eq.mpr, Even, id, congrArg, Eq.symm, propext, even_iff_two_dvd, Iff, Nat.even_sub, Nat.one_le_pow, Nat.Prime.pos, Fact.out, iff_of_false, ne_of_gt, Iff.mp, Nat.Prime.even_iff, And.left, Ne, And and 27 more

    95 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

  5. theorem Dickson.n_p_gt_one_of_psl_order line 149 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, HPow.hPow, Eq, Nat.card and 6 more

    Proof uses: Decidable.byContradiction, Not, Exists, False, Iff.mp, Fintype.card_eq_one_iff, LT.lt, Fintype.card_pos, Subgroup.Normal, Subgroup.Normal.mk, Eq.rec, HSMul.hSMul, Inv.inv, Subgroup.mem_map_of_mem, MonoidHom, MulAut, Monoid.End, MulDistribMulAction.toMonoidEnd, MulAut.conj, Dvd.dvd and 127 more

    188 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

    Open to load the checked before-and-after goal states.

  6. theorem Dickson.n_p_eq_psl line 183 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, Eq, Nat.card, HDiv.hDiv and 7 more

    Proof uses: Fact.out, Dvd.dvd, Eq.mpr, Even, id, congrArg, Eq.symm, propext, even_iff_two_dvd, Iff, Nat.even_sub, Nat.one_le_pow, Nat.le_trans, Nat.succ, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, LT.lt.le and 144 more

    187 instances, coercions and auxiliary constants left out.

    Tactic trace: 51 steps

    Open to load the checked before-and-after goal states.

  7. theorem Dickson.z1_eq_psl line 229 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, HPow.hPow, Eq, Nat.card and 7 more

    Proof uses: Subgroup.normalizer, Eq.mpr, id, congrArg, mul_comm, Eq.symm, Nat.card_eq_fintype_card, Subgroup.index, Sylow.card_eq_index_normalizer, Set, Sylow.coe_coe, Subgroup.index_mul_card, Eq.refl, HAdd.hAdd, Dickson.n_p_eq_psl, Nat.div_div_eq_div_mul, Nat.succ, Nat.mul_div_cancel, Nat.zero_lt_succ, pow_mul and 10 more

    81 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

    Open to load the checked before-and-after goal states.

  8. theorem Dickson.normDilationParam_image_card_eq_normalizerQuotient line 252 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Subgroup.map and 10 more

    Proof uses: MonoidHom, Units, MonoidHom.mk', Units.mk0, Dickson.dilationParam_ne_zero, Dickson.normalizer_element_fixes_infinity, Subtype.property, Units.ext, HMul.hMul, Dickson.normDilationParam_mul, MonoidHom.ker, Subgroup.comap, Subgroup.ext, Iff.intro, Inv.inv, Dickson.same_normDilationParam_imp_coset, Eq.trans, congr_arg, Eq.symm, Dickson.dilationParam and 33 more

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

    Open to load the checked before-and-after goal states.

  9. theorem Dickson.normalizer_dilation_params_cover_nq_roots line 290 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Subgroup.map and 14 more

    Proof uses: Set.range, Dickson.normDilationParam, Set.ncard, Dickson.normDilationParam_image_card_eq_normalizerQuotient, Set.Finite, Set.finite_range, Finset, Set.Finite.toFinset, Dickson.finite_subgroup_eq_roots_of_unity, Nat.div_pos, Nat.le_of_dvd, Nat.card_pos, Subgroup.card_dvd_of_le, Subgroup.le_normalizer, Eq.mpr, Finset.card, id, congrArg, Eq.symm, Set.ncard_coe_finset and 20 more

    101 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

    Open to load the checked before-and-after goal states.

  10. theorem Dickson.translationSet_stable_under_half_roots line 326 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, HPow.hPow, Eq, Nat.card and 13 more

    Proof uses: Eq.mpr, id, congrArg, And, Subgroup.normalizer, Exists, Dickson.normalizer_dilation_params_cover_nq_roots, Eq.mp, Dickson.normalizerQuotient, Eq.symm, Dickson.z1_eq_psl, Dickson.n_p_gt_one_of_psl_order

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  11. theorem Dickson.translationSet_scaled_eq_Fq_psl line 346 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, GE.ge, HPow.hPow, Set, Dickson.K, Eq, Set.ncard, Membership.mem, HAdd.hAdd, ZMod, HDiv.hDiv, HSub.hSub, Ne, HMul.hMul, Set.image, Inv.inv and 1 more

    Proof uses: Function.Injective, mul_right_injective₀, inv_ne_zero, Dickson.additive_subgroup_eq_F_q_from_squares, Eq.trans, Set.ncard_image_of_injective, And, Exists.intro, And.intro, mul_add, MulZeroClass.mul_zero, inv_mul_cancel₀, mul_left_comm

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.

  12. theorem Dickson.orbit_eq_infty_union_translations_psl line 364 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, HPow.hPow, Eq, Nat.card and 18 more

    Proof uses: Set.ncard, Eq.mpr, Fintype.card, Dickson.instFintypeSylow, id, congrArg, Dickson.orbitInfty_ncard, Dickson.n_p_eq_psl, Dickson.n_p_gt_one_of_psl_order, add_comm, Disjoint, Not, propext, Set.disjoint_singleton_left, And, False, Units, Matrix.vecCons, Matrix.vecEmpty, Exists and 34 more

    171 instances, coercions and auxiliary constants left out.

    Tactic trace: 35 steps

    Open to load the checked before-and-after goal states.

  13. theorem Dickson.orbit_infty_eq_P1Fq_psl_core line 406 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, HPow.hPow, Eq, Nat.card and 19 more

    Proof uses: Set.ncard, Fintype.card, Dickson.instFintypeSylow, Dickson.orbitInfty_ncard, Dickson.P1point, Ne, Set.exists_ne_of_one_lt_ncard, Eq.rec, Dickson.n_p_gt_one_of_psl_order, Eq.symm, Or, Dickson.projLine_cases, absurd, Eq.refl, Exists.intro, Dickson.translationSet, rfl, Eq.mpr, id, congrArg and 49 more

    132 instances, coercions and auxiliary constants left out.

    Tactic trace: 34 steps

    Open to load the checked before-and-after goal states.

  14. theorem Dickson.orbit_infty_eq_P1Fq_psl line 461 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, HPow.hPow, Eq, Nat.card and 13 more

    Proof uses: Dvd.dvd, Eq.mpr, Even, id, congrArg, Eq.symm, propext, even_iff_two_dvd, Iff, Nat.even_sub, Nat.one_le_pow, Nat.le_trans, Nat.succ, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, LT.lt.le, Fact.out and 59 more

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

    Open to load the checked before-and-after goal states.

  15. theorem Dickson.G_preserves_P1Fq_psl line 498 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, HPow.hPow, Eq, Nat.card and 13 more

    Proof uses: Dickson.orbitInfty, Dickson.orbit_infty_eq_P1Fq_psl, Exists.intro, Eq.rec, Dickson.preserves_orbitInfty, Eq.symm

    77 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  16. theorem Dickson.psl_G_le_pgl_range_from_orbit line 509 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, HPow.hPow, Eq, Nat.card and 14 more

    Proof uses: Dickson.ProjectiveLine, Set, Dickson.P1Fq, HSMul.hSMul, Dickson.G_preserves_P1Fq_psl, Exists.intro, Dickson.preserves_P1Fq_in_range

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.