OAI/AlgebraicGeometry/StableCoordinate/SourcePresentation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The polynomial presentation in the canonical obstruction interface

  1. def OAI.StableCoordinate.Obstruction.sourcePresentation line 15

    Source documentation

    The exact canonical source hypersurface is the four-variable polynomial ring.

    def sourcePresentation : A ℂ ≃ₐ[ℂ] StableCoordinate.R 4 :=
…

    Mentions: OAI.StableCoordinate.Obstruction.A, OAI.StableCoordinate.R

  2. theorem OAI.StableCoordinate.Obstruction.sourcePresentation_p line 18
  3. instance OAI.StableCoordinate.Obstruction.(instance at line 21) line 21
  4. instance OAI.StableCoordinate.Obstruction.(instance at line 24) line 24
  5. theorem OAI.StableCoordinate.Obstruction.f_coordinate_iff_source_coordinate line 31

    Source documentation

    Coordinateness of the exact polynomial is equivalent to coordinateness of the distinguished element in the source presentation, with arbitrary ambient coordinate changes on both sides.

    theorem f_coordinate_iff_source_coordinate :
    IsCoordinate (by decide : 0 < 4) StableCoordinate.f ↔
      ∃ e : A ℂ ≃ₐ[ℂ] StableCoordinate.R 4, e (aX ℂ 0) = MvPolynomial.X 0 := by
…

    Mentions: OAI.StableCoordinate.IsCoordinate, OAI.StableCoordinate.f, OAI.StableCoordinate.Obstruction.A, OAI.StableCoordinate.R, OAI.StableCoordinate.Obstruction.aX