OAI/AlgebraicGeometry/CommutingDerivations/ExtendedParameterRetraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The explicit intersection proof retains every dimension n >= 4 and identifies its ordinary polynomial side with the standard subalgebra C[F_n].

  1. def OAI.AbhyankarSathaye.CommutingDerivations.extendedAmbientParameter line 12
  2. def OAI.AbhyankarSathaye.CommutingDerivations.extendedParameterSlice line 15
  3. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedParameterSlice_rename line 19
  4. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedParameterSlice_parameter line 35
  5. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedParameterSlice_aeval line 41
  6. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedParameterSlice_aeval_apply line 47
  7. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedParameter_aeval_injective line 51
  8. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedParameter_ne_zero line 59
  9. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedParameter_power_saturated line 64
  10. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedParameter_localization_injective line 79
  11. theorem OAI.AbhyankarSathaye.CommutingDerivations.exists_aeval_add_one_iff line 89

    Source documentation

    Replacing f by f+1 does not change the literal polynomial-expression set.

    theorem exists_aeval_add_one_iff {K A : Type*} [CommRing K] [CommRing A] [Algebra K A]
    (f a : A) :
    (∃ q : Polynomial K, a = Polynomial.aeval (f + 1) q) ↔
      ∃ q : Polynomial K, a = Polynomial.aeval f q := by
…
  12. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedParameter_laurent_intersection line 104

    Source documentation

    Complete dimension-quantified intersection in the standard subalgebra representation of C[F_n], with localization membership given by one Laurent denominator and an ordinary polynomial numerator.

    theorem extendedParameter_laurent_intersection {n : ℕ} (hn : 4 ≤ n)
    (L : Type*) [CommRing L] [Algebra (MvPolynomial (Fin n) ℂ) L]
    [IsLocalization.Away (extendedAmbientParameter hn) L] (a : MvPolynomial (Fin n) ℂ) :
    (∃ (m : ℕ) (q : Polynomial ℂ),
      (algebraMap (MvPolynomial (Fin n) ℂ) L (extendedAmbientParameter hn))^m *
          algebraMap (MvPolynomial (Fin n) ℂ) L a =
        algebraMap (MvPolynomial (Fin n) ℂ) L (Polynomial.aeval (extendedAmbientParameter hn) q)) ↔
    a ∈ Algebra.adjoin ℂ ({extendedF hn} : Set (MvPolynomial (Fin n) ℂ)) := by
…

    Mentions: OAI.AbhyankarSathaye.CommutingDerivations.extendedAmbientParameter, OAI.AbhyankarSathaye.extendedF