SourceCoordinateTransport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Literal-polynomial coordinate systems in the canonical source algebra

The source presentation carries exactly aX 0 to the prescribed polynomial f. This reverses the presentation equivalence so a hypothetical coordinate automorphism of the literal four-variable polynomial gives precisely the coordinate-system direction used by the leading-derivation construction. No ambient automorphism is restricted or excluded.

theorem OAI.StableCoordinate.Obstruction.f_coordinate_iff_source_coordinate_system line 22
Source documentation
The exact coordinate predicate is equivalent to a polynomial coordinate system on the canonical source algebra, with its first coordinate equal to p. The equivalence quantifies over all ambient polynomial automorphisms.
```
theorem f_coordinate_iff_source_coordinate_system :
    IsCoordinate (by decide : 0 < 4) StableCoordinate.f ↔
      ∃ e : StableCoordinate.R 4 ≃ₐ[ℂ] A ℂ, e (X 0) = aX ℂ 0 := by
…
```
Mentions: OAI.StableCoordinate.IsCoordinate, OAI.StableCoordinate.f, OAI.StableCoordinate.R, OAI.StableCoordinate.Obstruction.A, OAI.StableCoordinate.Obstruction.aX
theorem OAI.StableCoordinate.Obstruction.source_coordinate_system_of_f_coordinate line 34
Source documentation
A four-variable coordinate for the literal polynomial supplies the actual source-coordinate equivalence needed by the negative proof.
```
theorem source_coordinate_system_of_f_coordinate
    (h : IsCoordinate (by decide : 0 < 4) StableCoordinate.f) :
    ∃ e : StableCoordinate.R 4 ≃ₐ[ℂ] A ℂ, e (X 0) = aX ℂ 0 :=
…
```
Mentions: OAI.StableCoordinate.IsCoordinate, OAI.StableCoordinate.f, OAI.StableCoordinate.R, OAI.StableCoordinate.Obstruction.A, OAI.StableCoordinate.Obstruction.aX