ReesPunctureTopology.lean`

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ReesProj.structuralMap_mem line 11
lemma OAI.ReesProj.chartSection_relation line 17
lemma OAI.ReesProj.preimage_basicOpen_le_chart line 26
Source documentation
Away from a chosen source section, the entire blowup belongs to the corresponding distinguished projective chart.
```
lemma preimage_basicOpen_le_chart (i : ι) :
    (structuralMap (sectionIdeal s)) ⁻¹ᵁ (PrimeSpectrum.basicOpen (s i)) ≤
      Proj.basicOpen (homogeneous (sectionIdeal s)) (chartSection s i) := by
…
```
Mentions: OAI.ReesProj.structuralMap, OAI.ReesProj.sectionIdeal, OAI.ReesProj.homogeneous, OAI.ReesProj.chartSection
lemma OAI.FractionalAlgebraAway.awayMap_eq_equiv line 60
theorem OAI.FractionalAlgebraAway.specMap_restrict_isIso line 73
Source documentation
A fraction-generated algebra gives the actual isomorphism over the principal open, including the structural morphism.
```
theorem specMap_restrict_isIso :
    IsIso ((Spec.map (CommRingCat.ofHom (algebraMap R B))) ∣_
      (PrimeSpectrum.basicOpen t)) := by
…
```
lemma OAI.SchemeRestrictionImage.openImmersion_restrict_isIso line 91
lemma OAI.SchemeRestrictionImage.isIso_of_chart line 107
Source documentation
If an open chart contains the entire preimage of a target open, an isomorphism for its composite is an isomorphism for the original map.
```
lemma isIso_of_chart {X Y Z : Scheme} (g : X ⟶ Y) (f : Y ⟶ Z)
    [IsOpenImmersion g] (U : Z.Opens)
    (hU : f ⁻¹ᵁ U ≤ g.opensRange) [IsIso ((g ≫ f) ∣_ U)] : IsIso (f ∣_ U) := by
…
```
lemma OAI.SchemeRestrictionImage.isIso_restrict_iSup line 117
Source documentation
Being an isomorphism over each member of a family is enough over its union, with no quasi-compactness or finiteness assumption.
```
lemma isIso_restrict_iSup {X Y : Scheme} (f : X ⟶ Y) {ι : Type}
    (U : ι → Y.Opens) (hU : ∀ i, IsIso (f ∣_ U i)) : IsIso (f ∣_ iSup U) := by
…
```
lemma OAI.ReesProj.fractionChartInclusion_opensRange line 150
theorem OAI.ReesProj.structuralMap_restrict_section_isIso line 169
Source documentation
The actual proper Rees-Proj morphism is an isomorphism over every source principal open belonging to its ideal of sections.
```
theorem structuralMap_restrict_section_isIso :
    IsIso ((structuralMap (sectionIdeal s)) ∣_ (PrimeSpectrum.basicOpen (s i))) := by
…
```
Mentions: OAI.ReesProj.structuralMap, OAI.ReesProj.sectionIdeal
theorem OAI.ReesProj.structuralMap_restrict_union_isIso line 188
Source documentation
The ordinary blowup is canonically the identity off the vanishing set of its nonzero chosen source sections.
```
theorem structuralMap_restrict_union_isIso (hs : ∀ j, s j ≠ 0) :
    IsIso ((structuralMap (sectionIdeal s)) ∣_
      (⨆ j, PrimeSpectrum.basicOpen (s j))) := by
…
```
Mentions: OAI.ReesProj.structuralMap, OAI.ReesProj.sectionIdeal
def OAI.ExplicitCone.completedPunctureOpen line 202
Source documentation
The open punctured spectrum is defined by the eighteen literal source sections; its complement is proved to be precisely the closed point.
```
def completedPunctureOpen : (Spec (.of completedRing)).Opens :=
…
```
Mentions: OAI.ExplicitCone.completedRing
theorem OAI.ExplicitCone.completedPunctureOpen_coe line 205
instance OAI.ExplicitCone.completedBlowupMap_puncture_isIso line 213
Source documentation
The actual proper eighteen-section Rees blowup is an isomorphism over the entire punctured spectrum, not just on a distinguished point or chart.
```
instance completedBlowupMap_puncture_isIso :
    IsIso (completedBlowupMap ∣_ completedPunctureOpen) :=
…
```
Mentions: OAI.ExplicitCone.completedBlowupMap, OAI.ExplicitCone.completedPunctureOpen
def OAI.ExplicitCone.completedBlowupPunctureIso line 217
lemma OAI.ExplicitCone.completedBlowupPunctureIso_hom_ι line 224
Source documentation
This isomorphism is the restriction of the fixed proper structural morphism of the actual completed-cone blowup.
```
lemma completedBlowupPunctureIso_hom_ι :
    completedBlowupPunctureIso.hom ≫ completedPunctureOpen.ι =
      (completedBlowupMap ⁻¹ᵁ completedPunctureOpen).ι ≫ completedBlowupMap :=
…
```
Mentions: OAI.ExplicitCone.completedBlowupMap, OAI.ExplicitCone.completedPunctureOpen
lemma OAI.ProjDomain.stalk_domain line 237
def OAI.ProjDomain.genericPoint line 247
Source documentation
A nonzero positive homogeneous element makes (0) a genuine point of Proj.
```
def genericPoint (f : A) {n : ℕ} (hn : n ≠ 0) (hf : f ∈ 𝒜 n) (hfn : f ≠ 0) : Proj 𝒜 where
…
```
lemma OAI.ProjDomain.genericPoint_specializes line 257
theorem OAI.ProjDomain.integral line 265
Source documentation
Integrality of the literal Proj of a domain; no smoothness assumption.
```
theorem integral (f : A) {n : ℕ} (hn : n ≠ 0) (hf : f ∈ 𝒜 n) (hfn : f ≠ 0) :
    IsIntegral (Proj 𝒜) := by
…
```
theorem OAI.ProperLocal.specializes_closedFiber line 285
Source documentation
Every point of a proper model over a local ring specializes to a point of its closed fiber.
```
theorem specializes_closedFiber (x : X) :
    ∃ y : X, x ⤳ y ∧ f y = IsLocalRing.closedPoint R := by
…
```
theorem OAI.ProperLocal.property_of_closedFiber line 297
Source documentation
A property stable under generalization and true on the closed fiber holds on the proper model over a local ring.
```
theorem property_of_closedFiber (P : X → Prop)
    (hgen : ∀ {x y}, x ⤳ y → P y → P x)
    (hfiber : ∀ y, f y = IsLocalRing.closedPoint R → P y) : ∀ x, P x := by
…
```
instance OAI.ExplicitCone.completedBlowup_locallyNoetherian line 309
lemma OAI.ExplicitCone.completedBlowupSection_ne_zero line 313
instance OAI.ExplicitCone.completedBlowup_integral line 321
Source documentation
The projective Rees modification is integral.
```
instance completedBlowup_integral : IsIntegral completedBlowup :=
…
```
Mentions: OAI.ExplicitCone.completedBlowup
theorem OAI.ExplicitCone.completedBlowup_specializes_closedFiber line 327
Source documentation
Every point of the actual model specializes into its closed fiber.
```
theorem completedBlowup_specializes_closedFiber (x : completedBlowup) :
    ∃ y : completedBlowup, x ⤳ y ∧ completedBlowupMap y = completedClosedPoint :=
…
```
Mentions: OAI.ExplicitCone.completedBlowup, OAI.ExplicitCone.y, OAI.ExplicitCone.completedBlowupMap, OAI.ExplicitCone.completedClosedPoint
theorem OAI.ExplicitCone.completedBlowup_closedFiber_nonempty line 339
Source documentation
The closed fiber of the actual proper modification is nonempty; this is proved from properness and integrality, not supplied as model data.
```
theorem completedBlowup_closedFiber_nonempty :
    ∃ x : completedBlowup, completedBlowupMap x = completedClosedPoint := by
…
```
Mentions: OAI.ExplicitCone.completedBlowup, OAI.ExplicitCone.completedBlowupMap, OAI.ExplicitCone.completedClosedPoint
theorem OAI.ExplicitCone.completedBlowupMap_surjective line 347
Source documentation
The genuine model covers the entire completed local spectrum, including the closed point. The puncture is the literal isomorphism already proved.
```
theorem completedBlowupMap_surjective : Function.Surjective completedBlowupMap := by
…
```
Mentions: OAI.ExplicitCone.completedBlowupMap
lemma OAI.ReesProj.homogeneousChartInclusion_structuralMap line 376
Source documentation
The literal homogeneous affine chart, as a scheme over the base ring.
```
lemma homogeneousChartInclusion_structuralMap :
    Proj.awayι (homogeneous I) (linearSection I t ht)
      (linearSection_homogeneous I t ht) (by decide : 0 < (1 : ℕ)) ≫ structuralMap I =
    Spec.map (CommRingCat.ofHom
      (@algebraMap R (homogeneousChart I t ht) _ _ (homogeneousChartScalarAlgebra I t ht))) := by
…
```
Mentions: OAI.ReesProj.homogeneous, OAI.ReesProj.linearSection, OAI.ReesProj.linearSection_homogeneous, OAI.ReesProj.structuralMap, OAI.ReesProj.homogeneousChart, OAI.ReesProj.homogeneousChartScalarAlgebra
abbrev OAI.ExplicitCone.completedChartInclusion line 396
Source documentation
The actual open embedding of the distinguished homogeneous Rees chart.
```
abbrev completedChartInclusion : Spec (.of completedBlowupChart) ⟶ completedBlowup :=
…
```
Mentions: OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowup
instance OAI.ExplicitCone.completedChartInclusion_open line 400
lemma OAI.ExplicitCone.completedChartInclusion_map line 408
Source documentation
The intrinsic Proj chart is over the fixed completed ring by precisely its scalar map, with actual equality of scheme morphisms.
```
lemma completedChartInclusion_map :
    completedChartInclusion ≫ completedBlowupMap =
      Spec.map (CommRingCat.ofHom (algebraMap completedRing completedBlowupChart)) :=
…
```
Mentions: OAI.ExplicitCone.completedChartInclusion, OAI.ExplicitCone.completedBlowupMap, OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedBlowupChart