Theorems · Definition · commutative algebra

wittStructureInt

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

wittStructureInt Φ is a family of polynomials ℕ → MvPolynomial (idx × ℕ) ℤ that are uniquely characterised by the property that `` bind₁ (wittStructureInt 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 wittStructureInt Φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials. See wittStructureInt_prop for this property, and wittStructureInt_existsUnique for the fact that wittStructureInt` gives the unique family of polynomials with this property.

Defined in

Mathlib.RingTheory.WittVector.StructurePolynomial

Cited by

13 results in Mathlib

Foundations

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

Assumes

Fact