OAI/GroupTheory/PolycyclicRecognition/Analysis/AffinePolynomialTopology.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The polynomial topology on finite affine coordinates

Points are embedded into the prime spectrum by their evaluation kernels. This gives a Noetherian T1 topology on finitely many field coordinates. Polynomial coordinate maps are continuous. This is the topology needed for the finite-component argument for linear groups.

  1. structure OAI.PolycyclicRecognition.AffinePolynomialPoint line 18
  2. def OAI.PolycyclicRecognition.AffinePolynomialPoint.toPrime line 25
  3. instance OAI.PolycyclicRecognition.AffinePolynomialPoint.(instance at line 28) line 28
  4. theorem OAI.PolycyclicRecognition.AffinePolynomialPoint.inducing_toPrime line 31
  5. theorem OAI.PolycyclicRecognition.AffinePolynomialPoint.toPrime_injective line 34
  6. instance OAI.PolycyclicRecognition.AffinePolynomialPoint.(instance at line 46) line 46
  7. instance OAI.PolycyclicRecognition.AffinePolynomialPoint.(instance at line 59) line 59
  8. def OAI.PolycyclicRecognition.AffinePolynomialPoint.polynomialMap line 62
  9. theorem OAI.PolycyclicRecognition.AffinePolynomialPoint.toPrime_polynomialMap line 66
  10. theorem OAI.PolycyclicRecognition.AffinePolynomialPoint.continuous_polynomialMap line 76
  11. theorem OAI.PolycyclicRecognition.AffinePolynomialPoint.isClosed_zeroSet line 85