ConcreteKernelIntersection.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The Laurent coefficient-map image intersects the ambient ring in exactly ℂ[F], by the explicit parameter retraction.

theorem OAI.AbhyankarSathaye.CommutingDerivations.polynomialCoefficientMap_apply line 13
theorem OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap_polynomial line 19
theorem OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap_complex_intersection line 28
Source documentation
Constants in the actual Laurent coefficient algebra have the prescribed complex scalar image in the actual ambient localization.
```
@[simp] theorem coefficientMap_complex_intersection (a : ℂ) :
    coefficientMap (algebraMap ℂ LaurentCoefficients a) = algebraMap ℂ LocalizedAmbient a := by
…
```
Mentions: OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap, OAI.AbhyankarSathaye.CommutingDerivations.LaurentCoefficients, OAI.AbhyankarSathaye.CommutingDerivations.LocalizedAmbient
theorem OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap_intersection line 36
Source documentation
Literal common-kernel intersection form: membership in the image of the actual coefficient map is equivalent to an ordinary polynomial in F.
```
theorem coefficientMap_intersection (r : R) :
    (∃ a : LaurentCoefficients, loc r = coefficientMap a) ↔
      ∃ q : Polynomial ℂ, r = Polynomial.aeval F q := by
…
```
Mentions: OAI.AbhyankarSathaye.R, OAI.AbhyankarSathaye.CommutingDerivations.LaurentCoefficients, OAI.AbhyankarSathaye.CommutingDerivations.loc, OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap, OAI.AbhyankarSathaye.F
theorem OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap_intersection_adjoin line 62