OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteCommutingOperatorAlgebra.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.commuting_adjoin_isMulCommutative line 17
2. theorem OAI.PolycyclicRecognition.commuting_adjoin_finite line 24
3. def OAI.PolycyclicRecognition.commutingOperatorEval line 33

   Source documentation

   Evaluate commuting operators by passing through their commutative generated algebra.

   def commutingOperatorEval (K : Type) [CommRing K] {E : Type} [Ring E] [Algebra K E]
       {k : ℕ} (s : Fin k → E) (h : ∀ i j, Commute (s i) (s j)) :
       MvPolynomial (Fin k) K →ₐ[K] E := by
   …

4. theorem OAI.PolycyclicRecognition.commutingOperatorEval_X line 41
5. theorem OAI.PolycyclicRecognition.relation_quotient_independent_bound line 55

   Source documentation

   Relations in a finite algebra bound every independent family in a quotient of any of its finitely generated subalgebras. No domain assumption on C is needed.

   theorem relation_quotient_independent_bound {r k n : ℕ}
       (a : Fin r → R) (ha : Algebra.adjoin K (Set.range a) = ⊤)
       [Module.Finite R C] (f : MvPolynomial (Fin k) K →ₐ[K] C)
       (β : MvPolynomial (Fin k) K →ₐ[K] B) (hβ : Function.Surjective β)
       (hker : ∀ p, f p = 0 → β p = 0)
       (x : Fin n → B) (hx : AlgebraicIndependent K x) : n ≤ r := by
   …