Theorems · Definition · commutative algebra

wittStructureRat

(p : ℕ) → {idx : Type u_2} → [hp : Fact (Nat.Prime p)] → MvPolynomial idx ℚ → ℕ → MvPolynomial (idx × ℕ) ℚ

wittStructureRat Φ is a family of polynomials ℕ → MvPolynomial (idx × ℕ) ℚ that are uniquely characterised by the property that `` bind₁ (wittStructureRat p Φ) (wittPolynomial p ℚ n) = bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℚ n))) Φ ` In other words: evaluating the n-th Witt polynomial on the family wittStructureRat Φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials. See wittStructureRat_prop for this property, and wittStructureRat_existsUnique for the fact that wittStructureRat gives the unique family of polynomials with this property. These polynomials turn out to have integral coefficients, but it requires some effort to show this. See wittStructureInt for the version with integral coefficients, and map_wittStructureInt for the fact that it is equal to wittStructureRat` when mapped to polynomials over the rationals.

Defined in

Mathlib.RingTheory.WittVector.StructurePolynomial

Cited by

12 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact