GeometricInterpretation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Schemes of the complex hypersurface fibers

An algebraic isomorphism of fiber coordinate rings induces an isomorphism of affine schemes over Spec ℂ. Nonrectifiability excludes every ambient scheme automorphism over the complex base, for each complex parameter.

abbrev OAI.StableCoordinate.GeometricInterpretation.Ambient line 24
Source documentation
The complex affine four-space in its standard spectrum presentation.
```
abbrev Ambient := Spec (CommRingCat.of (R 4))
```
Mentions: OAI.StableCoordinate.R
abbrev OAI.StableCoordinate.GeometricInterpretation.Fiber line 27
Source documentation
The fiber as a scheme, with its full coordinate-ring structure.
```
abbrev Fiber (t : ℂ) := Spec (CommRingCat.of (FiberRing t))
```
Mentions: OAI.StableCoordinate.FiberRing
def OAI.StableCoordinate.GeometricInterpretation.fiberEmbedding line 30
Source documentation
The actual closed immersion defined by f - t.
```
def fiberEmbedding (t : ℂ) : Fiber t ⟶ Ambient :=
…
```
Mentions: OAI.StableCoordinate.GeometricInterpretation.Fiber, OAI.StableCoordinate.GeometricInterpretation.Ambient
instance OAI.StableCoordinate.GeometricInterpretation.fiberEmbedding_isClosedImmersion line 33
def OAI.StableCoordinate.GeometricInterpretation.ambientAffineSpaceIso line 38
Source documentation
Standard identification of the ambient spectrum with affine four-space.
```
def ambientAffineSpaceIso :
    Ambient ≅ AffineSpace (Fin 4) (Spec (CommRingCat.of ℂ)) :=
…
```
Mentions: OAI.StableCoordinate.GeometricInterpretation.Ambient
def OAI.StableCoordinate.GeometricInterpretation.hyperplaneIdeal line 43
Source documentation
The coordinate hyperplane's defining ideal.
```
def hyperplaneIdeal : Ideal (R 4) := Ideal.span {X 0}
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.GeometricInterpretation.hyperplaneIdeal_isPrime line 45
theorem OAI.StableCoordinate.GeometricInterpretation.fiberIdeal_isPrime_of_affineFiber line 51
Source documentation
The fiber algebra condition proves its defining ideal is prime; this is not an additional hypothesis about the source polynomial.
```
theorem fiberIdeal_isPrime_of_affineFiber (t : ℂ) (h : IsAffineThreeSpaceFiber t) :
    (fiberIdeal t).IsPrime := by
…
```
Mentions: OAI.StableCoordinate.IsAffineThreeSpaceFiber, OAI.StableCoordinate.fiberIdeal
def OAI.StableCoordinate.GeometricInterpretation.IsSchemeRectifiableFiber line 59
Source documentation
Geometric rectifiability of the embedded image by an arbitrary ambient scheme automorphism over the complex base scheme.
```
def IsSchemeRectifiableFiber (t : ℂ) : Prop :=
…
```
theorem OAI.StableCoordinate.GeometricInterpretation.rectifiableFiber_iff_schemeRectifiable line 69
Source documentation
The defining-ideal orbit formulation captures exactly the geometric orbit condition under all ambient automorphisms. Radicality follows from the specified fiber algebra isomorphism, and is therefore not a new principal assumption.
```
theorem rectifiableFiber_iff_schemeRectifiable (t : ℂ)
    (h : IsAffineThreeSpaceFiber t) :
    IsRectifiableFiber t ↔ IsSchemeRectifiableFiber t := by
…
```
Mentions: OAI.StableCoordinate.IsAffineThreeSpaceFiber, OAI.StableCoordinate.IsRectifiableFiber, OAI.StableCoordinate.GeometricInterpretation.IsSchemeRectifiableFiber
theorem OAI.StableCoordinate.GeometricInterpretation.affineFiber_gives_schemeIso line 79
Source documentation
The fiber condition produces an isomorphism with affine three-space in the category of schemes over Spec ℂ, not only an equivalence of sets.
```
theorem affineFiber_gives_schemeIso (t : ℂ) (h : IsAffineThreeSpaceFiber t) :
    Nonempty (AffineGeometry.algebraSpec ℂ (FiberRing t) ≅
      Over.mk (AffineSpace (Fin 3) (Spec (CommRingCat.of ℂ)) ↘
        Spec (CommRingCat.of ℂ))) := by
…
```
Mentions: OAI.StableCoordinate.IsAffineThreeSpaceFiber, OAI.StableCoordinate.AffineGeometry.algebraSpec, OAI.StableCoordinate.FiberRing
theorem OAI.StableCoordinate.GeometricInterpretation.fiberPackage_gives_geometric_conclusion line 88
Source documentation
The full algebraic fiber package entails the full all-fiber geometric conclusion, including closed immersion and nonrectifiability of its image.
```
theorem fiberPackage_gives_geometric_conclusion (h : FiberPackage) :
    ∀ t : ℂ,
      Nonempty (AffineGeometry.algebraSpec ℂ (FiberRing t) ≅
        Over.mk (AffineSpace (Fin 3) (Spec (CommRingCat.of ℂ)) ↘
          Spec (CommRingCat.of ℂ))) ∧
      IsClosedImmersion (fiberEmbedding t) ∧
      ¬ IsSchemeRectifiableFiber t := by
…
```
Mentions: OAI.StableCoordinate.FiberPackage, OAI.StableCoordinate.AffineGeometry.algebraSpec, OAI.StableCoordinate.FiberRing, OAI.StableCoordinate.GeometricInterpretation.fiberEmbedding, OAI.StableCoordinate.GeometricInterpretation.IsSchemeRectifiableFiber