AffineModelRank.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ExplicitCone.completedChartBaseMap line 13
Source documentation
The genuine structure map of the distinguished affine chart of the literal eighteen-section ordinary blowup.
```
abbrev completedChartBaseMap : CommRingCat.of completedRing ⟶
    CommRingCat.of completedBlowupChart :=
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedBlowupChart
lemma OAI.ExplicitCone.completedChartBaseMap_injective line 17
instance OAI.ExplicitCone.completedBlowupExceptional_domain line 28
instance OAI.ExplicitCone.completedBlowupExceptional_prime line 32
lemma OAI.ExplicitCone.completedBlowupParameter_regular line 36
abbrev OAI.ExplicitCone.completedChartRestrictionSections line 43
Source documentation
The exceptional-chart module is the restriction of the double dual of the pullback module to a prime Cartier divisor.
```
abbrev completedChartRestrictionSections (M : ModuleCat.{0} completedRing) :=
…
```
Mentions: OAI.ExplicitCone.completedRing
theorem OAI.ExplicitCone.completedChartRestriction_torsionFree line 54
Source documentation
Torsion freedom is proved for the concrete exceptional module, not assumed as input to a numerical argument. There is no grading on M.
```
theorem completedChartRestriction_torsionFree (M : ModuleCat.{0} completedRing)
    [Module.Finite completedRing M] :
    Module.IsTorsionFree (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedChartRestrictionSections M) :=
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter, OAI.ExplicitCone.completedChartRestrictionSections
theorem OAI.ExplicitCone.completedChartRestriction_rank_pos line 62
Source documentation
A nonzero finite torsion-free module gives positive rank on the exceptional affine section chart.
```
theorem completedChartRestriction_rank_pos (M : ModuleCat.{0} completedRing)
    [Module.Finite completedRing M] [Module.IsTorsionFree completedRing M] [Nontrivial M] :
    0 < Module.finrank (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedChartRestrictionSections M) := by
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter, OAI.ExplicitCone.completedChartRestrictionSections
abbrev OAI.ExplicitCone.completedModelE line 80
Source documentation
The literal double-dual extension for an arbitrary module on the completed cone, on the genuine proper Rees modification constructed above. This is not an assumed object with prescribed numerical invariants.
```
abbrev completedModelE (M : ModuleCat completedRing) : completedBlowup.Modules :=
…
```
Mentions: OAI.ExplicitCone.completedRing
theorem OAI.ExplicitCone.completedModelE_coherent line 85
Source documentation
Coherence for EVERY finite module of the completed ring: no grading, algebra structure, or freeness premise is imposed on M.
```
theorem completedModelE_coherent (M : ModuleCat completedRing)
    [Module.Finite completedRing M] : (completedModelE M).IsFinitePresentation := by
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedModelE
theorem OAI.ExplicitCone.completedModelE_torsionFree line 92
Source documentation
Torsion freeness of the literal extension, proved on all open-section modules of the fixed integral model. No source regularity is assumed.
```
theorem completedModelE_torsionFree (M : ModuleCat completedRing)
    (U : completedBlowup.Opens) :
    @Module.IsTorsionFree Γ(completedBlowup, U)
      ((completedModelE M).val.obj (Opposite.op U)) _ _
      ((completedModelE M).val.obj (Opposite.op U)).isModule :=
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedBlowup, OAI.ExplicitCone.completedModelE

theorem OAI.ExplicitCone.completedModel_firstDual_coherent line 100

Source documentation

The first dual in the same construction is also genuinely coherent.

theorem completedModel_firstDual_coherent (M : ModuleCat completedRing)
    [Module.Finite completedRing M] :
    (CoherentDual.homSheaf completedBlowup.sheaf
      ((Scheme.Modules.pullback completedBlowupMap).obj (tilde M))
      (SheafOfModules.unit _)).IsFinitePresentation := by
…

Mentions: OAI.ExplicitCone.completedRing, OAI.CoherentDual.homSheaf, OAI.ExplicitCone.completedBlowupMap

abbrev OAI.ExplicitCone.completedExceptionalChartMap line 120
Source documentation
The literal prime Cartier divisor in the distinguished actual blowup chart, embedded into the GLOBAL proper model.
```
abbrev completedExceptionalChartMap :
    Spec (.of (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})) ⟶
      completedBlowup :=
…
```
Mentions: OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter, OAI.ExplicitCone.completedBlowup
abbrev OAI.ExplicitCone.completedGlobalRestrictionSections line 127
Source documentation
Sections of the restriction of the GLOBALLY defined extension E.
```
abbrev completedGlobalRestrictionSections (M : ModuleCat.{0} completedRing) :=
…
```
Mentions: OAI.ExplicitCone.completedRing
def OAI.ExplicitCone.completedGlobalRestrictionIso line 134
Source documentation
Compatibility with the actual global model; this closes the local/global identity left separate in the preceding positive-rank chart calculation.
```
def completedGlobalRestrictionIso (M : ModuleCat.{0} completedRing) :
    completedGlobalRestrictionSections M ≅ completedChartRestrictionSections M := by
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedGlobalRestrictionSections, OAI.ExplicitCone.completedChartRestrictionSections
theorem OAI.ExplicitCone.completedGlobalRestriction_torsionFree line 148
Source documentation
The actual global extension restricts to a torsion-free module along this whole exceptional chart, not merely its generic point.
```
theorem completedGlobalRestriction_torsionFree (M : ModuleCat.{0} completedRing)
    [Module.Finite completedRing M] :
    Module.IsTorsionFree (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedGlobalRestrictionSections M) := by
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter, OAI.ExplicitCone.completedGlobalRestrictionSections
theorem OAI.ExplicitCone.completedGlobalRestriction_rank_pos line 157
Source documentation
The restriction of the global double-dual extension has positive rank for every nonzero finite torsion-free module.
```
theorem completedGlobalRestriction_rank_pos (M : ModuleCat.{0} completedRing)
    [Module.Finite completedRing M] [Module.IsTorsionFree completedRing M] [Nontrivial M] :
    0 < Module.finrank (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedGlobalRestrictionSections M) := by
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter, OAI.ExplicitCone.completedGlobalRestrictionSections