OAI/GroupTheory/PolycyclicRecognition/Algebra/RingTraceProjectivity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A norm-one element makes a ring coefficient projective

For a finite group acting on a ring which is projective over the integers, an element with trace one gives an equivariant lift by averaging. Unlike rational averaging, no division by the group order is used.

  1. abbrev OAI.PolycyclicRecognition.ringActionRepresentation line 17
  2. def OAI.PolycyclicRecognition.ringTraceLift line 20
  3. theorem OAI.PolycyclicRecognition.ringTraceLift_equivariant line 35
  4. def OAI.PolycyclicRecognition.ringTraceLiftHom line 48
  5. theorem OAI.PolycyclicRecognition.ringTraceLiftHom_comp line 54
  6. theorem OAI.PolycyclicRecognition.ringAction_projective_of_trace_one line 75