AffineNormalization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Constant affine changes of polynomial coordinates

The automorphisms in this file normalize a nonzero scalar multiple of a coordinate and a constant translate. They are actual algebra automorphisms of the whole polynomial ring, with explicit polynomial inverses.

def OAI.StableCoordinate.affineAll line 24
Source documentation
Simultaneously replace every variable X i by a * X i + b.
```
noncomputable def affineAll (a b : k) (ha : a ≠ 0) :
    MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k :=
…
```
theorem OAI.StableCoordinate.affineAll_X line 42
theorem OAI.StableCoordinate.affineAll_C line 47
theorem OAI.StableCoordinate.affineAll_symm_X line 52
Source documentation
Its inverse removes the scalar and translate from every variable.
```
@[simp] theorem affineAll_symm_X (a b : k) (ha : a ≠ 0) (i : σ) :
    (affineAll (σ := σ) a b ha).symm (X i) = C a⁻¹ * (X i - C b) := by
…
```
Mentions: OAI.StableCoordinate.affineAll

theorem OAI.StableCoordinate.exists_equiv_eq_X_of_affine line 59

Source documentation

An ambient algebra automorphism taking a polynomial to an affine-linear coordinate can be normalized to take it to that variable exactly.

theorem exists_equiv_eq_X_of_affine
    (p : MvPolynomial σ k) (i : σ) (a b : k) (ha : a ≠ 0)
    (φ : MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k)
    (hφ : φ p = C a * X i + C b) :
    ∃ ψ : MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k, ψ p = X i := by
…

theorem OAI.StableCoordinate.exists_equiv_eq_X_of_sub_eq_scalar_mul line 70

Source documentation

The normalization needed after identifying the generators of two principal hypersurface ideals.

theorem exists_equiv_eq_X_of_sub_eq_scalar_mul
    (p : MvPolynomial σ k) (i : σ) (t a : k) (ha : a ≠ 0)
    (φ : MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k)
    (hφ : φ (p - C t) = C a * X i) :
    ∃ ψ : MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k, ψ p = X i := by
…

theorem OAI.StableCoordinate.isCoordinate_of_equiv_sub_eq_scalar_mul_X line 83
Source documentation
Specialized normalization for the exact IsCoordinate definition.
```
theorem isCoordinate_of_equiv_sub_eq_scalar_mul_X
    {n : ℕ} (hn : 0 < n) (p : R n) (t a : ℂ) (ha : a ≠ 0)
    (φ : R n ≃ₐ[ℂ] R n)
    (hφ : φ (p - C t) = C a * X ⟨0, hn⟩) :
    IsCoordinate hn p :=
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.IsCoordinate
theorem OAI.StableCoordinate.isCoordinate_sub_C_iff line 91
Source documentation
A constant translate does not alter whether a polynomial is a coordinate.
```
theorem isCoordinate_sub_C_iff {n : ℕ} (hn : 0 < n) (p : R n) (t : ℂ) :
    IsCoordinate hn (p - C t) ↔ IsCoordinate hn p := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.IsCoordinate