OAI/GroupTheory/BooneHigman/SteinbergLimits.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Steinberg sequential limits, annihilated kernels, and injective torus maps.

  1. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.transition_injective line 16
  2. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.of_injective line 26
  3. abbrev OAI.FiniteAlgebraicEnvelopes.Steinberg.ElementaryGroup line 41
  4. def OAI.FiniteAlgebraicEnvelopes.Steinberg.elementaryQuotient line 44
  5. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementaryQuotient_surjective line 46
  6. def OAI.FiniteAlgebraicEnvelopes.Steinberg.correctedUnits line 49
  7. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.correctedUnits_injective line 51
  8. def OAI.FiniteAlgebraicEnvelopes.Steinberg.elementaryTransition line 61
  9. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementaryTransition_injective line 69
  10. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary_natural line 75
  11. def OAI.FiniteAlgebraicEnvelopes.Steinberg.limitEquivalence line 80
  12. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.freshThird line 95
  13. def OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientSubring line 105

    Source documentation

    Ring coefficients whose root elements belong to a subgroup form a subring. The rank-six third index is used in the multiplication step.

    def coefficientSubring (H : Subgroup (Group (Fin 6) R))
    (h1 : ∀ i j (hij : i≠j), root i j hij (1:R)∈H) : Subring R where
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.root

  14. abbrev OAI.FiniteAlgebraicEnvelopes.Steinberg.RootIndex line 125
  15. def OAI.FiniteAlgebraicEnvelopes.Steinberg.rootGenerators line 127
  16. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.rootGenerators_finite line 130
  17. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.root_mem_generators line 133
  18. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.rootGenerators_generate line 137
  19. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.finitelyGenerated_of_ringGenerators line 153
  20. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.ringGenerators_of_algebraGenerators line 159
  21. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.thirdIndex line 178
  22. def OAI.FiniteAlgebraicEnvelopes.Steinberg.ringRelators line 186
  23. def OAI.FiniteAlgebraicEnvelopes.Steinberg.ringKernel line 189
  24. instance OAI.FiniteAlgebraicEnvelopes.Steinberg.(instance at line 190) line 190
  25. abbrev OAI.FiniteAlgebraicEnvelopes.Steinberg.RingQuotientGroup line 191
  26. def OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientRoot line 193
  27. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientRoot_add line 196
  28. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientRoot_chain line 201
  29. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientRoot_rel line 206
  30. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientRoot_congr line 215
  31. def OAI.FiniteAlgebraicEnvelopes.Steinberg.ringQuotRoot line 233
  32. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.ringQuotRoot_mk line 236
  33. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.ringQuotRoot_add line 241
  34. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.ringQuotRoot_chain line 247
  35. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.ringQuotRoot_distant line 253
  36. def OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientBackward line 261
  37. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientBackward_root line 276
  38. def OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientForward line 279
  39. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientForward_quotientRoot line 288
  40. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientForward_backward line 292
  41. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.quotientBackward_forward line 300
  42. def OAI.FiniteAlgebraicEnvelopes.Steinberg.ringQuotEquivalence line 307
  43. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.ringRelators_finite line 313
  44. theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.ringQuot_finitelyPresented line 327

    Source documentation

    Finite ring equations require only finitely many additional Steinberg relators.

    theorem ringQuot_finitelyPresented (hr : {p : R×R | r p.1 p.2}.Finite)
    [_root_.Group.IsFinitelyPresented (Group (Fin 6) R)] :
    _root_.Group.IsFinitelyPresented (Group (Fin 6) (RingQuot r)) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group