NYLL
Module

exists_isProper_surjective_isOpenImmersion_comp_eq_of_isIntegral.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isIntegral
105 declarations indexed from sourceView source ↗

Module documentation

exists is Proper surjective is Open Immersion comp eq of is Integral

Imports22
  • Lean.Elab.Command
  • Mathlib.AlgebraicGeometry.AffineScheme
  • Mathlib.AlgebraicGeometry.FunctionField
  • Mathlib.AlgebraicGeometry.Cover.Open
  • Mathlib.AlgebraicGeometry.IdealSheaf.Basic
  • Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
  • Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
  • Mathlib.AlgebraicGeometry.Morphisms.FiniteType
  • Mathlib.AlgebraicGeometry.Morphisms.Immersion
  • Mathlib.AlgebraicGeometry.Morphisms.Proper
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
  • Mathlib.AlgebraicGeometry.Morphisms.Separated
  • Mathlib.AlgebraicGeometry.Noetherian
  • Mathlib.AlgebraicGeometry.Properties
  • Mathlib.AlgebraicGeometry.PullbackCarrier
  • Mathlib.RingTheory.FiniteType
  • Mathlib.RingTheory.Ideal.Quotient.Nilpotent
  • Mathlib.Tactic.Choose
  • Mathlib.Topology.Connected.Clopen
  • Mathlib.Topology.Irreducible
  • Nyll.SchemeTheory.ProjectiveSpace.Basic
  • Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_algHom_away_apply_ratio_eq
Imported by2

Declarations

abbrev

grading

L56 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.grading
Documentation

The standard grading on homogeneous coordinates.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
Lean source · statement
abbrev grading (A : Type u) [CommRing A] (n : ℕ)
abbrev

PP

L60 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.PP
Documentation

Projective space with the chosen coordinates.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
Lean source · statement
abbrev PP (A : Type u) [CommRing A] (n : ℕ) : Scheme.{u}
abbrev

W

L63 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.W
Documentation

The standard affine open for the zeroth coordinate.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
Lean source · statement
abbrev W (A : Type u) [CommRing A] (n : ℕ) : (PP A n).Opens
abbrev

awayι₀

L67 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.awayι₀
Documentation

The inclusion of the zeroth affine chart.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
Lean source · statement
abbrev awayι₀ (A : Type u) [CommRing A] (n : ℕ) :
    Spec (.of (Away (grading A n) (MvPolynomial.X (0 : Fin (n + 1))))) ⟶ PP A n
lemma

ι_comp_eq_isoSpec_hom

L75 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ι_comp_eq_isoSpec_hom
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Chart
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
Lean source · statement
lemma ι_comp_eq_isoSpec_hom (U : X.Opens) (hU : IsAffineOpen U) :
    U.ι ≫ f = hU.isoSpec.hom ≫ Spec.map (f.appLE ⊤ U le_top) ≫
      Spec.map (Scheme.ΓSpecIso (CommRingCat.of A)).inv
theorem

exists_chart

L82 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.exists_chart
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Chart
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
Lean source · statement
theorem exists_chart [LocallyOfFiniteType f] (U : X.Opens) (hU : IsAffineOpen U) :
    ∃ (n : ℕ) (c : (U : Scheme.{u}) ⟶
        Spec (.of (Away (grading A n) (MvPolynomial.X (0 : Fin (n + 1)))))),
      IsClosedImmersion c ∧ c ≫ awayι₀ A n ≫ ProjSpace.π A n = U.ι ≫ f
structure

ChartData

L130 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData
Documentation

A finite covering with closed embeddings into projective affine charts.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
Lean source · full declaration
structure ChartData where
  /-- The number of charts. -/
  m : ℕ
  /-- The covering open subsets. -/
  U : Fin m → X.Opens
  /-- Every chart is nonempty. -/
  hne : ∀ k, ((U k : X.Opens) : Set X).Nonempty
  /-- The charts cover the original scheme. -/
  hcov : ⨆ k, U k = ⊤
  /-- The dimensions of the ambient projective spaces. -/
  e : Fin m → ℕ
  /-- The closed embeddings into standard affine charts. -/
  c : ∀ k, ((U k : X.Opens) : Scheme.{u}) ⟶
    Spec (.of (Away (grading A (e k)) (MvPolynomial.X (0 : Fin (e k + 1)))))
  /-- Each chart map is a closed immersion. -/
  hc : ∀ k, IsClosedImmersion (c k)
  /-- The chart embeddings commute with the structure morphisms. -/
  hover : ∀ k, c k ≫ awayι₀ A (e k) ≫ ProjSpace.π A (e k) = (U k).ι ≫ f
theorem

nonempty_chartData

L151 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.nonempty_chartData
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
Lean source · statement
theorem nonempty_chartData [LocallyOfFiniteType f] [CompactSpace X] : Nonempty (ChartData f)
def

ι

L169 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ι
Documentation

The immersion of a covering chart into projective space.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
def ι (k : Fin D.m) : ((D.U k : X.Opens) : Scheme.{u}) ⟶ PP A (D.e k)
instance

(anonymous instance)

L171 ↗
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
instance (k : Fin D.m) : IsImmersion (D.ι k)
lemma

ι_comp_π

L173 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ι_comp_π
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma ι_comp_π (k : Fin D.m) : D.ι k ≫ ProjSpace.π A (D.e k) = (D.U k).ι ≫ f
lemma

range_ι_subset

L176 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.range_ι_subset
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma range_ι_subset (k : Fin D.m) : Set.range (D.ι k) ⊆ (W A (D.e k) : Set (PP A (D.e k)))
abbrev

PiS

L182 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.PiS
Documentation

The product of the projective spaces over the base.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
abbrev PiS : Scheme.{u}
abbrev

prπ

L185 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.prπ
Documentation

The structure morphism of the projective product.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
abbrev prπ : D.PiS ⟶ Spec (CommRingCat.of A)
abbrev

pr

L188 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.pr
Documentation

The projection to a chosen projective factor.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
abbrev pr (k : Fin D.m) : D.PiS ⟶ PP A (D.e k)
def

Ω

L191 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.Ω
Documentation

The inverse image of a standard affine chart under a product projection.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
def Ω (k : Fin D.m) : D.PiS.Opens
def

Uo

L194 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.Uo
Documentation

The common open subset of the covering charts.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
def Uo : X.Opens
lemma

Uo_le

L196 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.Uo_le
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma Uo_le (k : Fin D.m) : D.Uo ≤ D.U k
lemma

mem_Uo

L198 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.mem_Uo
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma mem_Uo {x : X} : x ∈ D.Uo ↔ ∀ k, x ∈ D.U k
def

g

L203 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.g
Documentation

The morphism from the common open subset to the projective product.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
def g : (D.Uo : Scheme.{u}) ⟶ D.PiS
lemma

g_comp_prπ

L207 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.g_comp_prπ
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma g_comp_prπ : D.g ≫ D.prπ = D.Uo.ι ≫ f
lemma

g_comp_pr

L209 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.g_comp_pr
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma g_comp_pr (k : Fin D.m) : D.g ≫ D.pr k = X.homOfLE (D.Uo_le k) ≫ D.ι k
abbrev

XP

L213 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.XP
Documentation

The product of the original scheme and the projective ambient scheme over the base.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
abbrev XP : Scheme.{u}
def

ψ

L216 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψ
Documentation

The graph morphism into the ambient product.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
def ψ : (D.Uo : Scheme.{u}) ⟶ D.XP
lemma

ψ_fst

L218 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψ_fst
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma ψ_fst : D.ψ ≫ pullback.fst f D.prπ = D.Uo.ι
lemma

ψ_snd

L219 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψ_snd
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma ψ_snd : D.ψ ≫ pullback.snd f D.prπ = D.g
instance

(anonymous instance)

L221 ↗
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
instance : IsImmersion D.ψ
abbrev

X'

L226 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.X'
Documentation

The scheme-theoretic image of the graph morphism.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
abbrev X' : Scheme.{u}
abbrev

α

L229 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.α
Documentation

The closed immersion of the scheme-theoretic image.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
abbrev α : D.X' ⟶ D.XP
abbrev

ψ'

L232 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψ'
Documentation

The graph morphism factored through its image.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
abbrev ψ' : (D.Uo : Scheme.{u}) ⟶ D.X'
lemma

ψ'_α

L234 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψ'_α
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma ψ'_α : D.ψ' ≫ D.α = D.ψ
def

π

L237 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.π
Documentation

The image projection to the original scheme.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
def π : D.X' ⟶ X
def

ιι

L240 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ιι
Documentation

The image projection to the projective ambient scheme.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
def ιι : D.X' ⟶ D.PiS
instance

(anonymous instance)

L242 ↗
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
instance : IsProper D.π
instance

(anonymous instance)

L243 ↗
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
instance [IsSeparated f] : IsSeparated D.ιι
lemma

π_comp_f

L245 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.π_comp_f
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma π_comp_f : D.π ≫ f = D.ιι ≫ D.prπ
lemma

ψ'_π

L248 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψ'_π
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma ψ'_π : D.ψ' ≫ D.π = D.Uo.ι
lemma

ψ'_ιι

L249 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψ'_ιι
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
lemma ψ'_ιι : D.ψ' ≫ D.ιι = D.g
def

V

L252 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.V
Documentation

The inverse image of an original covering chart.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Setup
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
attribute [scoped instance] ChartData.hc
namespace ChartData
variable {f} (D : ChartData f)
Lean source · statement
def V (k : Fin D.m) : D.X'.Opens
lemma

isNoetherian_X

L299 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isNoetherian_X
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsIntegral X] in
Lean source · statement
lemma isNoetherian_X (_D : ChartData f) : IsNoetherian X
instance

noetherianSpace_Uo

L304 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.noetherianSpace_Uo
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance noetherianSpace_Uo : NoetherianSpace (D.Uo : Scheme.{u})
instance

compactSpace_XP

L309 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.compactSpace_XP
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance compactSpace_XP : CompactSpace D.XP
lemma

Uo_nonempty

L314 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.Uo_nonempty
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [LocallyOfFiniteType f] [QuasiCompact f] in
Lean source · statement
lemma Uo_nonempty : ((D.Uo : X.Opens) : Set X).Nonempty
instance

nonempty_Uo

L330 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.nonempty_Uo
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance nonempty_Uo : Nonempty (D.Uo : Scheme.{u})
instance

isIntegral_Uo

L334 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isIntegral_Uo
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance isIntegral_Uo : IsIntegral (D.Uo : Scheme.{u})
instance

quasiCompact_ψ

L337 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.quasiCompact_ψ
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance quasiCompact_ψ : QuasiCompact D.ψ
instance

(anonymous instance)

L338 ↗
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance : IsOpenImmersion D.ψ'
instance

(anonymous instance)

L339 ↗
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance : IsDominant D.ψ'
instance

isReduced_X'

L341 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isReduced_X'
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance isReduced_X' : IsReduced D.X'
instance

irreducibleSpace_X'

L355 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.irreducibleSpace_X'
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance irreducibleSpace_X' : IrreducibleSpace D.X'
instance

isIntegral_X'

L361 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isIntegral_X'
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance isIntegral_X' : IsIntegral D.X'
instance

compactSpace_X'

L363 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.compactSpace_X'
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Instances
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance compactSpace_X' : CompactSpace D.X'
def

πk

L411 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.πk
Documentation

The restriction of the image projection to a covering chart.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def πk (k : Fin D.m) : (D.V k : Scheme.{u}) ⟶ (D.U k : X.Opens)
lemma

πk_ι

L415 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.πk_ι
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma πk_ι (k : Fin D.m) : D.πk k ≫ (D.U k).ι = (D.V k).ι ≫ D.π
def

ak

L418 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ak
Documentation

The chartwise projective map through the original scheme.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def ak (k : Fin D.m) : (D.V k : Scheme.{u}) ⟶ PP A (D.e k)
def

bk

L421 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.bk
Documentation

The chartwise projective map through the ambient scheme.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def bk (k : Fin D.m) : (D.V k : Scheme.{u}) ⟶ PP A (D.e k)
lemma

range_ψ'_subset_V

L425 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.range_ψ'_subset_V
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma range_ψ'_subset_V (k : Fin D.m) : Set.range D.ψ' ⊆ Set.range (D.V k).ι
def

ψk

L433 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψk
Documentation

The lift from the common open subset to an image chart.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def ψk (k : Fin D.m) : (D.Uo : Scheme.{u}) ⟶ (D.V k : Scheme.{u})
lemma

ψk_ι

L438 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψk_ι
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma ψk_ι (k : Fin D.m) : D.ψk k ≫ (D.V k).ι = D.ψ'
instance

(anonymous instance)

L440 ↗
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance (k : Fin D.m) : IsDominant (D.ψk k)
lemma

ψk_πk

L450 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ψk_πk
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma ψk_πk (k : Fin D.m) : D.ψk k ≫ D.πk k = X.homOfLE (D.Uo_le k)
theorem

ak_eq_bk

L454 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ak_eq_bk
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
theorem ak_eq_bk (k : Fin D.m) : D.ak k = D.bk k
lemma

pr_ιι_apply

L460 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.pr_ιι_apply
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
lemma pr_ιι_apply (k : Fin D.m) (x : D.X') (hx : x ∈ D.V k) :
    D.pr k (D.ιι x) = D.ι k (D.πk k ⟨x, hx⟩)
lemma

V_le_preimage_Ω

L466 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.V_le_preimage_Ω
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step1
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
lemma V_le_preimage_Ω (k : Fin D.m) : D.V k ≤ D.ιι ⁻¹ᵁ D.Ω k
def

ιΩ

L517 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ιΩ
Documentation

The restriction of the ambient map to its affine chart.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def ιΩ (k : Fin D.m) : (D.V k : Scheme.{u}) ⟶ (D.Ω k : Scheme.{u})
lemma

ιΩ_ι

L520 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ιΩ_ι
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
lemma ιΩ_ι (k : Fin D.m) : D.ιΩ k ≫ (D.Ω k).ι = (D.V k).ι ≫ D.ιι
abbrev

T

L523 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.T
Documentation

The product of an original chart and an ambient chart over the base.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
abbrev T (k : Fin D.m) : Scheme.{u}
def

mT

L526 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.mT
Documentation

The open immersion of the chartwise product.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def mT (k : Fin D.m) : D.T k ⟶ D.XP
instance

(anonymous instance)

L529 ↗
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance (k : Fin D.m) : IsOpenImmersion (D.mT k)
lemma

mT_fst

L533 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.mT_fst
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma mT_fst (k : Fin D.m) : D.mT k ≫ pullback.fst f D.prπ = pullback.fst _ _ ≫ (D.U
  k).ι
lemma

mT_snd

L538 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.mT_snd
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma mT_snd (k : Fin D.m) : D.mT k ≫ pullback.snd f D.prπ = pullback.snd _ _ ≫ (D.Ω
  k).ι
lemma

range_mT

L544 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.range_mT
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma range_mT (k : Fin D.m) : Set.range (D.mT k) =
    pullback.fst f D.prπ ⁻¹' (D.U k : Set X) ∩ pullback.snd f D.prπ ⁻¹' (D.Ω k : Set D.PiS)
def

tk

L549 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.tk
Documentation

The map from an image chart to the chartwise product.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def tk (k : Fin D.m) : (D.V k : Scheme.{u}) ⟶ D.T k
lemma

tk_mT

L553 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.tk_mT
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
lemma tk_mT (k : Fin D.m) : D.tk k ≫ D.mT k = (D.V k).ι ≫ D.α
instance

(anonymous instance)

L558 ↗
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance (k : Fin D.m) : IsClosedImmersion (D.tk k)
def

rk

L582 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.rk
Documentation

The lift of an ambient affine chart to a standard projective chart.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def rk (k : Fin D.m) : (D.Ω k : Scheme.{u}) ⟶
    Spec (.of (Away (grading A (D.e k)) (MvPolynomial.X (0 : Fin (D.e k + 1)))))
lemma

rk_awayι

L591 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.rk_awayι
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma rk_awayι (k : Fin D.m) : D.rk k ≫ awayι₀ A (D.e k) = (D.Ω k).ι ≫ D.pr k
abbrev

G

L595 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.G
Documentation

The pullback of the closed chart embedding.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
abbrev G (k : Fin D.m) : Scheme.{u}
def

tk'

L598 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.tk'
Documentation

The factorization of the image chart through the closed pullback.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def tk' (k : Fin D.m) : (D.V k : Scheme.{u}) ⟶ D.G k
abbrev

ik

L605 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ik
Documentation

The structure morphism of the standard projective chart.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
abbrev ik (k : Fin D.m) : Spec (.of (Away (grading A (D.e k)) (MvPolynomial.X (0 : Fin (D.e k +
  1)))))
    ⟶ Spec (CommRingCat.of A)
lemma

c_ik

L611 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.c_ik
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma c_ik (k : Fin D.m) : D.c k ≫ D.ik k = (D.U k).ι ≫ f
lemma

rk_ik

L615 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.rk_ik
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsIntegral X] [LocallyOfFiniteType f]
  [QuasiCompact f] in
Lean source · statement
lemma rk_ik (k : Fin D.m) : D.rk k ≫ D.ik k = (D.Ω k).ι ≫ D.prπ
lemma

tk'_comp

L618 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.tk'_comp
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
lemma tk'_comp (k : Fin D.m) :
    D.tk' k ≫ pullback.mapDesc (D.c k) (D.rk k) (D.ik k) ≫
      (pullback.congrHom (D.c_ik k) (D.rk_ik k)).hom = D.tk k
instance

(anonymous instance)

L627 ↗
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance (k : Fin D.m) : IsClosedImmersion (D.tk' k)
theorem

isClosedImmersion_ιΩ

L634 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isClosedImmersion_ιΩ
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step3
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
theorem isClosedImmersion_ιΩ (k : Fin D.m) : IsClosedImmersion (D.ιΩ k)
abbrev

O

L684 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.O
Documentation

The inverse image of an ambient affine chart.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step2
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
abbrev O (k : Fin D.m) : D.X'.Opens
abbrev

ek

L687 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ek
Documentation

The inclusion of an image chart into an ambient inverse image.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step2
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
abbrev ek (k : Fin D.m) : (D.V k : Scheme.{u}) ⟶ (D.O k : Scheme.{u})
lemma

ek_comp

L691 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ek_comp
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step2
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsSeparated f] in
Lean source · statement
lemma ek_comp (k : Fin D.m) : D.ek k ≫ (D.ιι ∣_ D.Ω k) = D.ιΩ k
lemma

V_nonempty

L694 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.V_nonempty
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step2
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsNoetherianRing A] [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] in
Lean source · statement
lemma V_nonempty (k : Fin D.m) : ((D.V k : D.X'.Opens) : Set D.X').Nonempty
instance

nonempty_O

L698 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.nonempty_O
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step2
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance nonempty_O (k : Fin D.m) : Nonempty (D.O k : Scheme.{u})
instance

isProper_ek

L702 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isProper_ek
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step2
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance isProper_ek (k : Fin D.m) : IsProper (D.ek k)
theorem

V_eq_O

L707 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.V_eq_O
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step2
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
theorem V_eq_O (k : Fin D.m) : D.V k = D.O k
instance

isClosedImmersion_restrict

L767 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isClosedImmersion_restrict
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance isClosedImmersion_restrict (k : Fin D.m) : IsClosedImmersion (D.ιι ∣_ D.Ω k)
def

Ωall

L779 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.Ωall
Documentation

The union of the ambient affine charts.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def Ωall : D.PiS.Opens
lemma

range_ιι_subset

L782 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.range_ιι_subset
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsSeparated f] in
Lean source · statement
lemma range_ιι_subset : Set.range D.ιι ⊆ Set.range D.Ωall.ι
def

ιall

L791 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ιall
Documentation

The factorization of the image map through the union of ambient charts.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
def ιall : D.X' ⟶ (D.Ωall : Scheme.{u})
lemma

ιall_ι

L794 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.ιall_ι
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
omit [IsSeparated f] in
Lean source · statement
lemma ιall_ι : D.ιall ≫ D.Ωall.ι = D.ιι
instance

isClosedImmersion_ιall

L796 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isClosedImmersion_ιall
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance isClosedImmersion_ιall : IsClosedImmersion D.ιall
instance

isImmersion_ιι

L814 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isImmersion_ιι
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance isImmersion_ιι : IsImmersion D.ιι
instance

isNoetherian_X'

L816 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.isNoetherian_X'
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance isNoetherian_X' : IsNoetherian D.X'
instance

quasiCompact_ιι

L823 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.quasiCompact_ιι
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance quasiCompact_ιι : QuasiCompact D.ιι
instance

surjective_π

L825 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.surjective_π
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
Lean source · statement
instance surjective_π : Surjective D.π
theorem

chow

L837 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.ChartData.chow
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
section Step4
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} [IsIntegral X]
  {f : X ⟶ Spec (CommRingCat.of A)} [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
  (D : ChartData f)
namespace ChartData
include D in
Lean source · statement
theorem chow : ∃ (X' P : Scheme.{u}) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A)),
    IsProper π ∧ Surjective π ∧ IsOpenImmersion j ∧ IsProper q ∧ j ≫ q = π ≫ f
theorem

main

L878 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Compactification.SolCHint.main
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace SolCHint
Lean source · statement
theorem main {A : Type u} [CommRing A] [IsNoetherianRing A]
    {X : Scheme.{u}} [IsIntegral X] (f : X ⟶ Spec (CommRingCat.of A))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] :
    ∃ (X' P : Scheme.{u}) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A)),
      IsProper π ∧ Surjective π ∧ IsOpenImmersion j ∧ IsProper q ∧ j ≫ q = π ≫ f
theorem

exists_isProper_surjective_isOpenImmersion_comp_eq_of_isIntegral

L926 ↗
AlgebraicGeometry.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isIntegral
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Compactification
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Topology
  HomogeneousLocalization
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isIntegral
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {X : Scheme.{u}} [IsIntegral X] (f : X ⟶ Spec (CommRingCat.of A))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] :
    ∃ (X' P : Scheme.{u}) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A)),
      IsProper π ∧ Surjective π ∧ IsOpenImmersion j ∧ IsProper q ∧ j ≫ q = π ≫ f

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.