OAI/RingTheory/GroupAction/TraceOne.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Trace ideals, trace one from free field-valued points, adic unit lifting and degree bounds.

  1. def OAI.DescentExponents.groupTrace line 18
  2. lemma OAI.DescentExponents.groupTrace_fixed line 20
  3. def OAI.DescentExponents.invariantTrace line 24
  4. lemma OAI.DescentExponents.invariantTrace_zero line 28
  5. lemma OAI.DescentExponents.invariantTrace_add line 32
  6. lemma OAI.DescentExponents.invariantTrace_mul line 37
  7. def OAI.DescentExponents.traceIdeal line 46
  8. lemma OAI.DescentExponents.trace_not_killed_by_free_point line 56
  9. theorem OAI.DescentExponents.algebraic_trace_one line 81
  10. lemma OAI.DescentExponents.map_groupTrace line 122
  11. theorem OAI.DescentExponents.unit_trace_of_complete_target line 127
  12. lemma OAI.DescentExponents.exponent_page_bound line 152
  13. lemma OAI.DescentExponents.exists_obstruction_power line 157
  14. lemma OAI.DescentExponents.exponent_page_bound_int line 162
  15. lemma OAI.DescentExponents.differential_index_range line 166
  16. lemma OAI.DescentExponents.outgoing_degree_equation line 180
  17. lemma OAI.DescentExponents.incoming_degree_equation line 188