GradedRelationSanity.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Elementary certificates for the graded hypersurface

The negative-coordinate proof uses localization away from p. This file establishes that p is regular in the actual graded hypersurface quotient, using the exact relation rather than a domain assumption. It also supplies localization-domain descent and nonvanishing certificates for the five specified homogeneous generators.

theorem OAI.StableCoordinate.GradedRelationSanity.quotient_mem_nonZeroDivisors line 27
Source documentation
A coefficient relatively prime to a principal relation stays regular modulo it.
```
theorem quotient_mem_nonZeroDivisors {h p : R} (hr : IsRelPrime h p) :
    Ideal.Quotient.mk (Ideal.span ({h} : Set R)) p ∈
      nonZeroDivisors (R ⧸ Ideal.span ({h} : Set R)) := by
…
```
Mentions: OAI.StableCoordinate.R

theorem OAI.StableCoordinate.GradedRelationSanity.quotient_away_injective line 38

Source documentation

Localization away from such a regular element is injective.

theorem quotient_away_injective {h p : R} (hr : IsRelPrime h p)
    (S : Type*) [CommRing S] [Algebra (R ⧸ Ideal.span ({h} : Set R)) S]
    [IsLocalization.Away (Ideal.Quotient.mk (Ideal.span ({h} : Set R)) p) S] :
    Function.Injective (algebraMap (R ⧸ Ideal.span ({h} : Set R)) S) := by
…

Mentions: OAI.StableCoordinate.R

theorem OAI.StableCoordinate.GradedRelationSanity.quotient_isDomain_of_away_isDomain line 48

Source documentation

Domain-ness descends from the localization, without assuming the quotient a domain.

theorem quotient_isDomain_of_away_isDomain {h p : R} (hr : IsRelPrime h p)
    (S : Type*) [CommRing S] [Algebra (R ⧸ Ideal.span ({h} : Set R)) S]
    [IsLocalization.Away (Ideal.Quotient.mk (Ideal.span ({h} : Set R)) p) S]
    [IsDomain S] : IsDomain (R ⧸ Ideal.span ({h} : Set R)) :=
…

Mentions: OAI.StableCoordinate.R

theorem OAI.StableCoordinate.GradedRelationSanity.p_not_dvd_Hstar line 64
Source documentation
p does not divide the displayed highest relation: specialize to (0,0,0,0,1).
```
theorem p_not_dvd_Hstar : ¬ (X 0 : P k 5) ∣ Hstar k := by
…
```
theorem OAI.StableCoordinate.GradedRelationSanity.Hstar_ne_zero line 70
Source documentation
The highest relation is a nonzero polynomial.
```
theorem Hstar_ne_zero : Hstar k ≠ 0 := by
…
```
theorem OAI.StableCoordinate.GradedRelationSanity.Hstar_relPrime_p line 77
Source documentation
The independent variable p is irreducible, hence relatively prime to Hstar.
```
theorem Hstar_relPrime_p : IsRelPrime (Hstar k) (X 0 : P k 5) := by
…
```
theorem OAI.StableCoordinate.GradedRelationSanity.gX_zero_mem_nonZeroDivisors line 85
Source documentation
The class of p is not a zero divisor in the ACTUAL quotient, before domain descent.
```
theorem gX_zero_mem_nonZeroDivisors : gX k 0 ∈ nonZeroDivisors (G k) :=
…
```

theorem OAI.StableCoordinate.GradedRelationSanity.G_away_injective line 89

Source documentation

The canonical map from G into its p-localization is injective.

theorem G_away_injective (S : Type*) [CommRing S] [Algebra (G k) S]
    [IsLocalization.Away (gX k 0) S] : Function.Injective (algebraMap (G k) S) := by
…

theorem OAI.StableCoordinate.GradedRelationSanity.G_isDomain_of_away_isDomain line 99
Source documentation
A domain certificate for the explicit localized model proves the original G a domain.
```
theorem G_isDomain_of_away_isDomain (S : Type*) [CommRing S] [Algebra (G k) S]
    [IsLocalization.Away (gX k 0) S] [IsDomain S] : IsDomain (G k) := by
…
```