OperatorNaturality.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.map_variableOperator line 15
Source documentation
Coefficient extension commutes with each differential or multiplication step.
```
theorem map_variableOperator (f : K →+* L) (isV : σ → Bool) (i : σ)
    (p : MvPolynomial σ K) :
    map f (variableOperator isV i p) = variableOperator isV i (map f p) := by
…
```
Mentions: OAI.Problem335.variableOperator
theorem OAI.Problem335.map_mixedOperator line 22
Source documentation
The full mixed operator is natural under every homomorphism of coefficient semirings. In particular its unnormalized integer matrix extends to any field.
```
theorem map_mixedOperator (f : K →+* L) (isV : σ → Bool)
    (p q : MvPolynomial σ K) :
    map f (mixedOperator isV p q) = mixedOperator isV (map f p) (map f q) := by
…
```
Mentions: OAI.Problem335.mixedOperator
def OAI.Problem335.mixedMonomialMatrix line 37
Source documentation
The coefficient matrix in arbitrary selected source and target monomials. When the selections enumerate bidegree fibers, this is the restricted operator matrix in the unnormalized monomial bases.
```
def mixedMonomialMatrix {I J : Type*} (isV : σ → Bool)
    (p : MvPolynomial σ K) (source : I → σ →₀ ℕ) (target : J → σ →₀ ℕ) :
    Matrix J I K :=
…
```
theorem OAI.Problem335.mixedMonomialMatrix_map line 42

theorem OAI.Problem335.integer_mixedMonomialMatrix_rank_eq line 54

Source documentation

Integral mixed operators have field-independent monomial-matrix rank in characteristic zero, with no embedding between the two fields required.

theorem integer_mixedMonomialMatrix_rank_eq
    {I J : Type*} [Fintype I] [Fintype J]
    (K L : Type*) [Field K] [CharZero K] [Field L] [CharZero L]
    (isV : σ → Bool) (p : MvPolynomial σ ℤ)
    (source : I → σ →₀ ℕ) (target : J → σ →₀ ℕ) :
    (mixedMonomialMatrix isV (map (Int.castRingHom K) p) source target).rank =
      (mixedMonomialMatrix isV (map (Int.castRingHom L) p) source target).rank := by
…

Mentions: OAI.Problem335.mixedMonomialMatrix