OAI/GroupTheory/PolycyclicRecognition/Algebra/PointwiseAlgebraicEndomorphism.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local polynomial relations on a finite module give an integral operator

  1. theorem OAI.PolycyclicRecognition.polynomialOrbit_exists_annihilator line 14
  2. theorem OAI.PolycyclicRecognition.integral_endomorphism_of_pointwise_relation line 41

    Source documentation

    The product of annihilators of a finite module generating set annihilates all vectors, because the operator commutes with the coefficient ring.

    theorem integral_endomorphism_of_pointwise_relation (T : Module.End R N)
    (h : ∀ v : N, ∃ p : K[X], p ≠ 0 ∧ Polynomial.aeval T p v = 0) :
    IsIntegral K T := by
…