OAI/LinearAlgebra/Descent/Rational.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Rational descent of automorphism-invariant subspaces

Over an algebraically closed field of characteristic zero, a coefficient-invariant subspace of finitely supported vectors is obtained by scalar extension from its rational intersection. The coordinate index set is arbitrary, and the intersection is given both as a pullback and as a literal subspace of the ambient space.

CoefficientStable is a hypothesis on an arbitrary subspace, not a definition of the Arthur filtration. The trace-defined Arthur filtration, its geometric setup and characteristic hypotheses, and coefficient independence for that filtration are not formalized here.

  1. theorem OAI.ArthurLinearDescent.exists_extension_ringAut line 23
  2. def OAI.ArthurLinearDescent.translateVariables line 52
  3. theorem OAI.ArthurLinearDescent.translateVariables_X line 59
  4. theorem OAI.ArthurLinearDescent.exists_move_transcendental line 63
  5. theorem OAI.ArthurLinearDescent.fixedField_rat line 97
  6. def OAI.ArthurLinearDescent.coefficientInclusion line 120
  7. theorem OAI.ArthurLinearDescent.coefficientInclusion_apply line 123
  8. def OAI.ArthurLinearDescent.coefficientIntersection line 126
  9. theorem OAI.ArthurLinearDescent.mem_coefficientIntersection line 129
  10. theorem OAI.ArthurLinearDescent.coefficientInclusion_injective line 132
  11. def OAI.ArthurLinearDescent.ambientIntersection line 139
  12. def OAI.ArthurLinearDescent.intersectionToAmbient line 142
  13. theorem OAI.ArthurLinearDescent.intersectionToAmbient_apply line 147
  14. def OAI.ArthurLinearDescent.intersectionEquiv line 151
  15. theorem OAI.ArthurLinearDescent.intersectionEquiv_apply line 165
  16. def OAI.ArthurLinearDescent.coefficientAction line 169
  17. theorem OAI.ArthurLinearDescent.coefficientAction_apply line 173
  18. def OAI.ArthurLinearDescent.CoefficientStable line 176
  19. theorem OAI.ArthurLinearDescent.elimination_support line 179
  20. theorem OAI.ArthurLinearDescent.minimal_support_fixed line 195
  21. theorem OAI.ArthurLinearDescent.span_fixedVectors line 226
  22. theorem OAI.ArthurLinearDescent.exists_preimage_coefficientInclusion line 275
  23. def OAI.ArthurLinearDescent.intersectionInclusion line 289
  24. def OAI.ArthurLinearDescent.naturalMap line 295
  25. theorem OAI.ArthurLinearDescent.naturalMap_tmul line 299
  26. def OAI.ArthurLinearDescent.ambientIntersectionInclusion line 303
  27. def OAI.ArthurLinearDescent.ambientNaturalMap line 308
  28. theorem OAI.ArthurLinearDescent.ambientNaturalMap_tmul line 312
  29. theorem OAI.ArthurLinearDescent.naturalMap_eq_ambientNaturalMap line 316
  30. theorem OAI.ArthurLinearDescent.subtype_naturalMap line 324
  31. theorem OAI.ArthurLinearDescent.naturalMap_injective line 335
  32. theorem OAI.ArthurLinearDescent.naturalMap_bijective_of_fixedField line 344
  33. def OAI.ArthurLinearDescent.naturalEquiv_of_fixedField line 370
  34. theorem OAI.ArthurLinearDescent.rational_descent line 378
  35. def OAI.ArthurLinearDescent.rationalDescentEquiv line 383
  36. theorem OAI.ArthurLinearDescent.rationalDescentEquiv_apply line 388
  37. theorem OAI.ArthurLinearDescent.rationalDescentEquiv_tmul line 394
  38. def OAI.ArthurLinearDescent.ambientRationalDescentEquiv line 401
  39. theorem OAI.ArthurLinearDescent.ambientRationalDescentEquiv_apply line 407
  40. theorem OAI.ArthurLinearDescent.ambient_rational_descent line 416