KummerCMRestriction.lean`

60 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExplicitCone.completedGlobalRestriction_of_depth_three line 17

Source documentation

The double dual of the pullback of a depth-three module has a nonzero torsion-free restriction to the exceptional affine chart.

theorem completedGlobalRestriction_of_depth_three
    (M : ModuleCat.{0} completedRing) [Module.Finite completedRing M] [Nontrivial M]
    (hdepth : SmallCM.localDepth completedRing M = 3) :
    Module.IsTorsionFree (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedGlobalRestrictionSections M) ∧
    0 < Module.finrank (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedGlobalRestrictionSections M) := by
…

Mentions: OAI.ExplicitCone.completedRing, OAI.SmallCM.localDepth, OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter, OAI.ExplicitCone.completedGlobalRestrictionSections

theorem OAI.ExplicitCone.actual_extension_of_CM_module line 29

Source documentation

The global double-dual extension is coherent and has positive-rank torsion-free restriction to the exceptional affine chart.

theorem actual_extension_of_CM_module
    (M : Type) [AddCommGroup M] [Module completedRing M]
    [Module.Finite completedRing M] [Nontrivial M]
    (hdepth : SmallCM.localDepth completedRing M = 3) :
    (completedModelE (ModuleCat.of completedRing M)).IsFinitePresentation ∧
    (∀ U : completedBlowup.Opens,
      @Module.IsTorsionFree Γ(completedBlowup, U)
        ((completedModelE (ModuleCat.of completedRing M)).val.obj (Opposite.op U)) _ _
        ((completedModelE (ModuleCat.of completedRing M)).val.obj (Opposite.op U)).isModule) ∧
    Module.IsTorsionFree (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedGlobalRestrictionSections (ModuleCat.of completedRing M)) ∧
    0 < Module.finrank (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
…

Mentions: OAI.ExplicitCone.completedRing, OAI.SmallCM.localDepth, OAI.ExplicitCone.completedModelE, OAI.ExplicitCone.completedBlowup, OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter, OAI.ExplicitCone.completedGlobalRestrictionSections

lemma OAI.PrincipalDivisorGeneric.local_dvr line 54
Source documentation
The generic local ring of a nonzero prime Cartier divisor really is a DVR. The ambient ring need not already be assumed regular.
```
lemma local_dvr (t : R) (ht : t ≠ 0) [(Ideal.span ({t} : Set R)).IsPrime] :
    IsDiscreteValuationRing (Localization.AtPrime (Ideal.span ({t} : Set R))) := by
…
```

lemma OAI.PrincipalDivisorGeneric.localized_free line 74

Source documentation

A finite torsion-free sheaf therefore has a free stalk at the divisor's generic point, as used in the manuscript's actual extension argument.

lemma localized_free (t : R) (ht : t ≠ 0) [(Ideal.span ({t} : Set R)).IsPrime]
    [Module.Finite R M] [Module.IsTorsionFree R M] :
    Module.Free (Localization.AtPrime (Ideal.span ({t} : Set R)))
      (LocalizedModule (Ideal.span ({t} : Set R)).primeCompl M) := by
…

lemma OAI.PrincipalDivisorGeneric.localized_rank line 83

Source documentation

Localization at the generic point preserves the module rank.

lemma localized_rank (p : Ideal R) [p.IsPrime] :
    Module.finrank (Localization.AtPrime p) (LocalizedModule p.primeCompl M) =
      Module.finrank R M := by
…

lemma OAI.PrincipalDivisorGeneric.exists_free_neighborhood line 93

Source documentation

A genuine open neighborhood (not only a stalk) of the generic divisor point has a free module, with the same generic rank as the ambient module.

lemma exists_free_neighborhood (t : R) (ht : t ≠ 0)
    [(Ideal.span ({t} : Set R)).IsPrime] [Module.Finite R M] [Module.IsTorsionFree R M] :
    ∃ s : R, s ∉ Ideal.span ({t} : Set R) ∧
      Module.Free (Localization (.powers s)) (LocalizedModule.Away s M) ∧
      Module.finrank (Localization (.powers s)) (LocalizedModule.Away s M) =
        Module.finrank R M := by
…

lemma OAI.PrincipalDivisorGeneric.residue_rank line 108

Source documentation

The generic fiber on the actual principal divisor has exactly the ambient generic rank, because its generic local ring is a DVR.

lemma residue_rank (t : R) (ht : t ≠ 0)
    [(Ideal.span ({t} : Set R)).IsPrime] [Module.Finite R M] [Module.IsTorsionFree R M] :
    Module.finrank (Ideal.span ({t} : Set R)).ResidueField
      ((Ideal.span ({t} : Set R)).ResidueField ⊗[R] M) = Module.finrank R M := by
…

lemma OAI.PrincipalDivisorGeneric.quotient_rank line 125
lemma OAI.DomainModuleRank.fraction_rank line 155
lemma OAI.DomainModuleRank.dual_rank line 163
Source documentation
The generic rank of an honest dual is the original generic rank. Finite presentation supplies Hom-localization, not a false global freeness.
```
lemma dual_rank [Module.FinitePresentation R M] :
    Module.finrank R (Module.Dual R M) = Module.finrank R M := by
…
```
lemma OAI.DomainModuleRank.baseChange_rank line 174
Source documentation
Injective scalar extension preserves generic rank even if it is not flat. The comparison is made over the two honest fraction fields.
```
lemma baseChange_rank (B : Type*) [CommRing B] [IsDomain B] [Algebra R B]
    (hinj : Function.Injective (algebraMap R B)) :
    Module.finrank B (B ⊗[R] M) = Module.finrank R M := by
…
```
lemma OAI.DomainModuleRank.doubleDual_rank line 189
lemma OAI.DomainModuleRank.doubleDual_baseChange_rank line 197
theorem OAI.CoherentModelActual.affineE_cartier_rank_eq line 223
Source documentation
Exact generic rank of the genuine double-dual model on a prime Cartier divisor. No flatness of the model over the source and no freeness of M is assumed. The source's original rank is retained through both duals and restriction at the generic divisor point.
```
theorem affineE_cartier_rank_eq (hf : Function.Injective f)
    (t : B) (ht : t ≠ 0) [(Ideal.span ({t} : Set B)).IsPrime] :
    let q : B ⟶ CommRingCat.of (B ⧸ Ideal.span ({t} : Set B)) :=
…
```
theorem OAI.ExplicitCone.completedChartRestriction_rank_eq line 254
Source documentation
Source paper.tex339–340: the generic rank of the actual restriction equals the ORIGINAL completed-cone module rank, not only an unspecified positive integer. This holds for arbitrary finite ungraded modules.
```
theorem completedChartRestriction_rank_eq (M : ModuleCat.{0} completedRing)
    [Module.Finite completedRing M] :
    Module.finrank (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedChartRestrictionSections M) = Module.finrank completedRing M := by
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter, OAI.ExplicitCone.completedChartRestrictionSections
theorem OAI.ExplicitCone.completedGlobalRestriction_rank_eq line 264
Source documentation
The comparison is made for the globally constructed coherent double dual E, using its honest restriction isomorphism with the affine model.
```
theorem completedGlobalRestriction_rank_eq (M : ModuleCat.{0} completedRing)
    [Module.Finite completedRing M] :
    Module.finrank (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedGlobalRestrictionSections M) = Module.finrank completedRing M := by
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter, OAI.ExplicitCone.completedGlobalRestrictionSections

theorem OAI.ExplicitCone.actual_extension_rank_of_CM_module line 272

Source documentation

The coherent double-dual extension has torsion-free restriction with the same generic rank as the original module.

theorem actual_extension_rank_of_CM_module
    (M : Type) [AddCommGroup M] [Module completedRing M]
    [Module.Finite completedRing M] [Nontrivial M]
    (hdepth : SmallCM.localDepth completedRing M = 3) :
    (completedModelE (ModuleCat.of completedRing M)).IsFinitePresentation ∧
    (∀ U : completedBlowup.Opens,
      @Module.IsTorsionFree Γ(completedBlowup, U)
        ((completedModelE (ModuleCat.of completedRing M)).val.obj (Opposite.op U)) _ _
        ((completedModelE (ModuleCat.of completedRing M)).val.obj (Opposite.op U)).isModule) ∧
    Module.IsTorsionFree (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
      (completedGlobalRestrictionSections (ModuleCat.of completedRing M)) ∧
    (Module.finrank (completedBlowupChart ⧸ Ideal.span {completedBlowupParameter})
…

lemma OAI.DomainModuleRank.tower_rank line 301
Source documentation
The field-degree rank formula for arbitrary modules in a finite-domain extension. Neither the ring extension nor the module is assumed free.
```
lemma tower_rank :
    Module.finrank A R * Module.finrank R M = Module.finrank A M := by
…
```
theorem OAI.ExplicitCone.completed_exceptional_rank_formula line 332
Source documentation
The free A-module rank of an arbitrary hypothetical CM module is the normalization degree times the rank of its TRUE exceptional restriction. This is an equality deduced from the constructed rings/maps/sheaf; the source surface equality deg(f)=H² remains a geometric identification.
```
theorem completed_exceptional_rank_formula
    (M : Type) [AddCommGroup M] [Module completedRing M] [Module.Finite completedRing M] :
    letI := Module.restrictScalars (MvPowerSeries (Fin 3) ℂ) completedRing M
…
```
Mentions: OAI.ExplicitCone.completedRing
lemma OAI.ExplicitCone.completed_parameter_degree_pos line 348
Source documentation
Positivity of the normalization degree, proved for the actual finite injective three-parameter power-series map.
```
lemma completed_parameter_degree_pos :
    0 < Module.finrank (MvPowerSeries (Fin 3) ℂ) completedRing := by
…
```
Mentions: OAI.ExplicitCone.completedRing
lemma OAI.GradedPolynomialMap.homogeneous_pow_le line 361
lemma OAI.GradedPolynomialMap.map_mem line 369

def OAI.GradedPolynomialMap.lift line 383

Source documentation

A degree-one substitution into a genuinely graded target is graded.

def lift (f : MvPolynomial σ k →ₐ[k] B)
    (hX : ∀ i, f (MvPolynomial.X i) ∈ ℬ 1) :
    MvPolynomial.homogeneousSubmodule σ k →ₐᵍ[k] ℬ :=
…

lemma OAI.GradedPolynomialMap.zero_component line 388
def OAI.AlgebraicGeometry.ProjectiveSpectrum.radical_comapFun line 427
Source documentation
The underlying function of Proj ℬ ⟶ Proj 𝒜 on the level of points.
```
@[simps] def radical_comapFun (p : ProjectiveSpectrum ℬ) : ProjectiveSpectrum 𝒜 where
…
```
def OAI.AlgebraicGeometry.ProjectiveSpectrum.radicalComap line 438
Source documentation
The underlying continuous function of Proj ℬ ⟶ Proj 𝒜 on the level of points.
```
def radicalComap : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜) where
…
```
def OAI.AlgebraicGeometry.Proj.radical_comapStructureSheafFun line 456
Source documentation
The underlying function of Proj ℬ ⟶ Proj 𝒜 on the level of structure sheaves.
```
noncomputable def radical_comapStructureSheafFun
    (s : ∀ x : U, AtPrime 𝒜 x.1.1.1) (y : V) : AtPrime ℬ y.1.1.1 :=
…
```
lemma OAI.AlgebraicGeometry.Proj.radical_isLocallyFraction_comapStructureSheafFun line 460
def OAI.AlgebraicGeometry.Proj.radical_comapStructureSheaf line 480
Source documentation
The underlying ring hom of Proj ℬ ⟶ Proj 𝒜 on the level of structure sheaves.
```
noncomputable def radical_comapStructureSheaf :
    (Proj.structureSheaf 𝒜).1.obj (.op U) →+* (Proj.structureSheaf ℬ).1.obj (.op V) where
…
```
def OAI.AlgebraicGeometry.Proj.radical_sheafedSpaceMap line 532
Source documentation
The underlying map of Proj ℬ ⟶ Proj 𝒜 on the level of sheafed spaces.
```
@[simps! (isSimp := false)] noncomputable def radical_sheafedSpaceMap :
…
```
lemma OAI.AlgebraicGeometry.Proj.radical_germ_map_sectionInBasicOpen line 542
lemma OAI.AlgebraicGeometry.Proj.radical_val_sectionInBasicOpen_apply line 552
theorem OAI.AlgebraicGeometry.Proj.radical_localRingHom_comp_stalkIso line 558

def OAI.AlgebraicGeometry.Proj.radicalMap line 583

Source documentation

Functoriality of Proj.

noncomputable def radicalMap : _root_.AlgebraicGeometry.Proj ℬ ⟶ _root_.AlgebraicGeometry.Proj 𝒜 where
…

theorem OAI.AlgebraicGeometry.Proj.radical_map_preimage_basicOpen line 600
theorem OAI.AlgebraicGeometry.Proj.radical_ι_comp_map line 603
lemma OAI.AlgebraicGeometry.Proj.radical_awayToSection_comp_appLE line 607

theorem OAI.AlgebraicGeometry.Proj.radical_awayι_comp_map line 630

Source documentation

The following square commutes:

Proj ℬ         ⟶ Proj 𝒜₁
    ^                   ^
    |                   |
Spec A₂[f(s)⁻¹]₀ ⟶ Spec A₁[s⁻¹]₀

@[reassoc] theorem radical_awayι_comp_map {i : ℕ} (hi : 0 < i) (s : A) (hs : s ∈ 𝒜 i) :
    _root_.AlgebraicGeometry.Proj.awayι ℬ (f s) (f.2 hs) hi ≫ radicalMap f hf =
    _root_.AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ _root_.AlgebraicGeometry.Proj.awayι 𝒜 s hs hi := by
…

Mentions: OAI.AlgebraicGeometry.Proj.radicalMap

lemma OAI.GradedIntegralProj.sub_zero_component line 673
lemma OAI.GradedIntegralProj.quotient_base_scalars line 682
lemma OAI.GradedIntegralProj.irrelevant_le_radical line 700
Source documentation
A finite/integral homogeneous normalization cannot acquire projective points above the vertex. Radical inclusion is DERIVED, not an extra map hypothesis. The connected degree-zero algebra is the ground field.
```
lemma irrelevant_le_radical (f : 𝒜 →ₐᵍ[k] ℬ)
    (hint : f.toAlgHom.toRingHom.IsIntegral)
    (hzero : ∀ a ∈ 𝒜 0, ∃ c : k, algebraMap k A c = a) :
    ℬ₊.toIdeal ≤ (𝒜₊.toIdeal.map f.toAlgHom.toRingHom).radical := by
…
```

def OAI.GradedIntegralProj.integralMap line 754

Source documentation

Actual projective scheme morphism induced by an integral homogeneous map of connected graded algebras.

def integralMap (f : 𝒜 →ₐᵍ[k] ℬ)
    (hint : f.toAlgHom.toRingHom.IsIntegral)
    (hzero : ∀ a ∈ 𝒜 0, ∃ c : k, algebraMap k A c = a) :
    Proj ℬ ⟶ Proj 𝒜 :=
…

theorem OAI.GradedIntegralProj.integralMap_chart line 760
def OAI.SectionCompletion.linearGradedMap line 782
Source documentation
The genuine degree-one Noether-normalization map, now with its grading.
```
def linearGradedMap : MvPolynomial.homogeneousSubmodule σ k →ₐᵍ[k] homogeneous T :=
…
```
Mentions: OAI.SectionCompletion.homogeneous
def OAI.SectionCompletion.linearProjectiveMap line 790
Source documentation
The actual projective morphism associated to a finite degree-one normalization. Finiteness is used to PROVE the radical irrelevant containment.
```
def linearProjectiveMap (hfin : (linearPolynomialMap T w hw).Finite) :
    proj T ⟶ Proj (MvPolynomial.homogeneousSubmodule σ k) :=
…
```
Mentions: OAI.SectionCompletion.linearPolynomialMap, OAI.SectionCompletion.proj
lemma OAI.SectionCompletion.linearProjectiveMap_chart line 796
lemma OAI.ExplicitCone.exists_finite_linear_projective_parameters line 813
Source documentation
Finite homogeneous normalization of the literal normalized Kummer cone, without substituting abstract numerical invariants for its rings.
```
lemma exists_finite_linear_projective_parameters :
    ∃ (w : Fin 3 → L) (hw : ∀ i, w i ∈ pieces 1),
      (SectionCompletion.linearPolynomialMap pieces w hw).Finite ∧
      Function.Injective (SectionCompletion.linearPolynomialMap pieces w hw) := by
…
```
Mentions: OAI.ExplicitCone.L, OAI.ExplicitCone.pieces, OAI.SectionCompletion.linearPolynomialMap
abbrev OAI.ExplicitCone.plane line 832
def OAI.ExplicitCone.projectiveParameter line 834
theorem OAI.ExplicitCone.projectiveParameter_mem line 836
lemma OAI.ExplicitCone.projectiveParameter_finite line 839
def OAI.ExplicitCone.projectiveNormalization line 846
Source documentation
Actual morphism X→P² from the precise normalized section cone. No claim identifying all of X with the source's smooth Kummer surface is included, and no finite W→V conclusion is assumed.
```
def projectiveNormalization : projectiveSurface ⟶ plane :=
…
```
Mentions: OAI.ExplicitCone.projectiveSurface, OAI.ExplicitCone.plane
def OAI.SectionCompletion.homogeneousChartAlgMap line 861
def OAI.SectionCompletion.evaluateInv line 865
lemma OAI.SectionCompletion.evaluateInv_homogeneous line 868
lemma OAI.SectionCompletion.evaluateInv_mem_range line 875
def OAI.SectionCompletion.dehomogenize line 886
Source documentation
Literal degree-one dehomogenization of the section algebra into its actual homogeneous affine Proj chart, constructed as an algebra map.
```
def dehomogenize : polynomials T →ₐ[k] homogeneousChart T c hc :=
…
```
Mentions: OAI.SectionCompletion.polynomials, OAI.SectionCompletion.homogeneousChart
lemma OAI.SectionCompletion.homogeneousChartMap_dehomogenize line 891
lemma OAI.SectionCompletion.dehomogenize_surjective line 899
Source documentation
Every homogeneous fraction is the dehomogenization of its numerator; this is not a flatness or geometric assumption.
```
lemma dehomogenize_surjective : Function.Surjective (dehomogenize T c hc hn) := by
…
```
Mentions: OAI.SectionCompletion.dehomogenize
lemma OAI.SectionCompletion.dehomogenize_linearSection line 907