PrincipalIdeal.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Principal hypersurface ideals over a field

The elementary algebraic interface used in the proof of cor:fibers is that two polynomials which generate the same ideal differ by a nonzero scalar. This module proves that statement and its transported form under algebra maps.

theorem OAI.StableCoordinate.eq_nonzero_scalar_mul_of_span_singleton_eq line 23
Source documentation
Equal principal ideals in a polynomial ring over a field have generators that differ by a nonzero scalar. This includes the zero ideal.
```
theorem eq_nonzero_scalar_mul_of_span_singleton_eq
    {f g : MvPolynomial σ k}
    (h : Ideal.span ({f} : Set (MvPolynomial σ k)) = Ideal.span {g}) :
    ∃ c : k, c ≠ 0 ∧ f = C c * g := by
…
```
Mentions: OAI.StableCoordinate.f

theorem OAI.StableCoordinate.span_singleton_eq_of_eq_nonzero_scalar_mul line 33

Source documentation

Scalar multiples by a nonzero field element generate the same ideal.

theorem span_singleton_eq_of_eq_nonzero_scalar_mul
    {f g : MvPolynomial σ k} {c : k} (hc : c ≠ 0) (h : f = C c * g) :
    Ideal.span ({f} : Set (MvPolynomial σ k)) = Ideal.span {g} := by
…

Mentions: OAI.StableCoordinate.f

theorem OAI.StableCoordinate.span_singleton_eq_iff_nonzero_scalar_mul line 40

Source documentation

A precise algebraic form of the generator normalization step.

theorem span_singleton_eq_iff_nonzero_scalar_mul
    {f g : MvPolynomial σ k} :
    Ideal.span ({f} : Set (MvPolynomial σ k)) = Ideal.span {g} ↔
      ∃ c : k, c ≠ 0 ∧ f = C c * g := by
…

Mentions: OAI.StableCoordinate.f

theorem OAI.StableCoordinate.map_span_singleton_algHom line 51
Source documentation
Images of principal ideals under algebra maps are generated by the image of the generator. No surjectivity assumption is needed.
```
theorem map_span_singleton_algHom
    {A B : Type*} [CommRing A] [CommRing B] [Algebra k A] [Algebra k B]
    (φ : A →ₐ[k] B) (f : A) :
    Ideal.map φ.toRingHom (Ideal.span ({f} : Set A)) = Ideal.span {φ f} := by
…
```
Mentions: OAI.StableCoordinate.f

theorem OAI.StableCoordinate.eq_nonzero_scalar_mul_of_map_span_singleton_eq line 60

Source documentation

If an algebra map takes a polynomial principal ideal to another principal ideal, its value on the generator is a nonzero scalar multiple of the target.

theorem eq_nonzero_scalar_mul_of_map_span_singleton_eq
    {τ : Type*} (φ : MvPolynomial σ k →ₐ[k] MvPolynomial τ k)
    {f : MvPolynomial σ k} {g : MvPolynomial τ k}
    (h : Ideal.map φ.toRingHom (Ideal.span ({f} : Set (MvPolynomial σ k))) =
      Ideal.span {g}) :
    ∃ c : k, c ≠ 0 ∧ φ f = C c * g := by
…

Mentions: OAI.StableCoordinate.f