NYLL
Module

CurveModel_isProper_smooth_places_affineCover_glued.lean

Nyll.AlgebraicCurves.Models.CurveModel_isProper_smooth_places_affineCover_glued
62 declarations indexed from sourceView source ↗

Module documentation

Curve Model is Proper smooth places affine Cover glued

Imports82
  • Nyll.AlgebraicCurves.Models.Construction
  • Nyll.AlgebraicCurves.Models.ChartAlgebra
  • Nyll.AlgebraicCurves.Models.Smoothness
  • Nyll.AlgebraicCurves.Divisors.ClassGroup
  • Mathlib.Algebra.Algebra.Basic
  • Mathlib.Algebra.Algebra.Tower
  • Mathlib.Algebra.GCDMonoid.IntegrallyClosed
  • Mathlib.Algebra.GroupWithZero.NonZeroDivisors
  • Mathlib.Algebra.Polynomial.AlgebraMap
  • Mathlib.Algebra.Polynomial.Basic
  • Mathlib.Algebra.Polynomial.Eval.Coeff
  • Mathlib.AlgebraicGeometry.AffineScheme
  • Mathlib.AlgebraicGeometry.FunctionField
  • Mathlib.AlgebraicGeometry.Gluing
  • Mathlib.AlgebraicGeometry.Morphisms.Basic
  • Mathlib.AlgebraicGeometry.Morphisms.FiniteType
  • Mathlib.AlgebraicGeometry.Morphisms.Proper
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
  • Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
  • Mathlib.AlgebraicGeometry.Morphisms.Smooth
  • Mathlib.AlgebraicGeometry.Noetherian
  • Mathlib.AlgebraicGeometry.OpenImmersion
  • Mathlib.AlgebraicGeometry.Scheme
  • Mathlib.AlgebraicGeometry.StructureSheaf
  • Mathlib.AlgebraicGeometry.ValuativeCriterion
  • Mathlib.CategoryTheory.Limits.HasLimits
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  • Mathlib.Data.Set.Finite.Basic
  • Mathlib.Data.Set.Finite.Lattice
  • Mathlib.Data.Set.Insert
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
  • Mathlib.FieldTheory.Perfect
  • Mathlib.FieldTheory.Separable
  • Mathlib.LinearAlgebra.Dimension.Basic
  • Mathlib.LinearAlgebra.Dimension.Constructions
  • Mathlib.LinearAlgebra.FiniteDimensional.Defs
  • Mathlib.RingTheory.Algebraic.Basic
  • Mathlib.RingTheory.Algebraic.Integral
  • Mathlib.RingTheory.DedekindDomain.AdicValuation
  • Mathlib.RingTheory.DedekindDomain.Basic
  • Mathlib.RingTheory.DedekindDomain.IntegralClosure
  • Mathlib.RingTheory.EssentialFiniteness
  • Mathlib.RingTheory.Etale.Field
  • Mathlib.RingTheory.Etale.Kaehler
  • Mathlib.RingTheory.Etale.Locus
  • Mathlib.RingTheory.FinitePresentation
  • Mathlib.RingTheory.FiniteType
  • Mathlib.RingTheory.Finiteness.Basic
  • Mathlib.RingTheory.Flat.TorsionFree
  • Mathlib.RingTheory.Ideal.Basic
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.Ideal.Prime
  • Mathlib.RingTheory.Ideal.Quotient.Basic
  • Mathlib.RingTheory.Ideal.Quotient.Defs
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.RingTheory.Ideal.Span
  • Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
  • Mathlib.RingTheory.Jacobson.Ring
  • Mathlib.RingTheory.Kaehler.Basic
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.Localization.Basic
  • Mathlib.RingTheory.Localization.Defs
  • Mathlib.RingTheory.Localization.Integral
  • Mathlib.RingTheory.Localization.LocalizationLocalization
  • Mathlib.RingTheory.Localization.Submodule
  • Mathlib.RingTheory.RingHom.Locally
  • Mathlib.RingTheory.RingHom.StandardSmooth
  • Mathlib.RingTheory.Smooth.Basic
  • Mathlib.RingTheory.Smooth.Fiber
  • Mathlib.RingTheory.Smooth.Field
  • Mathlib.RingTheory.Smooth.Locus
  • Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  • Mathlib.RingTheory.Smooth.StandardSmoothOfFree
  • Mathlib.RingTheory.Spectrum.Prime.Topology
  • Mathlib.RingTheory.Unramified.LocalRing
  • Mathlib.RingTheory.Unramified.Locus
  • Mathlib.RingTheory.Valuation.Basic
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.Tactic.Ring.RingNF
  • Mathlib.Topology.JacobsonSpace
  • Mathlib.Topology.Sober
Imported by3

Declarations

instance

locallyOfFiniteType_isZariskiLocalAtSource

L108 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.locallyOfFiniteType_isZariskiLocalAtSource
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
Lean source · statement
instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType)
theorem

adjoin_inv_eq_adjoin

L121 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.adjoin_inv_eq_adjoin
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section ChartRings
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
Lean source · statement
theorem adjoin_inv_eq_adjoin (t : L) : K⟮t⁻¹⟯ = K⟮t⟯
instance

finiteDimensional_adjoin_inv

L129 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.finiteDimensional_adjoin_inv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section ChartRings
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
Lean source · statement
instance finiteDimensional_adjoin_inv (t : L) [FiniteDimensional K⟮t⟯ L] :
    FiniteDimensional K⟮t⁻¹⟯ L
instance

isSeparable_adjoin_inv

L133 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.isSeparable_adjoin_inv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section ChartRings
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
Lean source · statement
instance isSeparable_adjoin_inv (t : L) [Algebra.IsSeparable K⟮t⟯ L] :
    Algebra.IsSeparable K⟮t⁻¹⟯ L
instance

isDedekindDomain_chartRing_of_isSeparable

L138 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.isDedekindDomain_chartRing_of_isSeparable
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section ChartRings
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
open scoped IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
instance isDedekindDomain_chartRing_of_isSeparable (s : L) [FiniteDimensional K⟮s⟯ L]
    [Algebra.IsSeparable K⟮s⟯ L] : IsDedekindDomain (chartRing K ({s} : Set L))
instance

finite_chartRing_of_isSeparable

L143 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.finite_chartRing_of_isSeparable
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section ChartRings
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
open scoped IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
instance finite_chartRing_of_isSeparable (s : L) [FiniteDimensional K⟮s⟯ L]
    [Algebra.IsSeparable K⟮s⟯ L] :
    Module.Finite (Algebra.adjoin K ({s} : Set L)) (chartRing K ({s} : Set L))
instance

finiteType_chartRing_of_isSeparable

L148 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.finiteType_chartRing_of_isSeparable
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section ChartRings
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
Lean source · statement
instance finiteType_chartRing_of_isSeparable (s : L) [FiniteDimensional K⟮s⟯ L]
    [Algebra.IsSeparable K⟮s⟯ L] : Algebra.FiniteType K (chartRing K ({s} : Set L))
instance

isNoetherianRing_chartRing_of_isSeparable

L154 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.isNoetherianRing_chartRing_of_isSeparable
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section ChartRings
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
Lean source · statement
instance isNoetherianRing_chartRing_of_isSeparable (s : L) [FiniteDimensional K⟮s⟯ L]
    [Algebra.IsSeparable K⟮s⟯ L] : IsNoetherianRing (chartRing K ({s} : Set L))
theorem

locallyOfFiniteType_gluedToBase_of_isSeparable

L164 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.locallyOfFiniteType_gluedToBase_of_isSeparable
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
Lean source · statement
theorem locallyOfFiniteType_gluedToBase_of_isSeparable [FiniteDimensional K⟮t⟯ L]
    [Algebra.IsSeparable K⟮t⟯ L] : LocallyOfFiniteType (gluedToBase K t)
theorem

isLocallyNoetherian_glued_of_isSeparable

L188 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.isLocallyNoetherian_glued_of_isSeparable
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
Lean source · statement
theorem isLocallyNoetherian_glued_of_isSeparable [FiniteDimensional K⟮t⟯ L]
    [Algebra.IsSeparable K⟮t⟯ L] : IsLocallyNoetherian (glued K t)
theorem

quasiSeparated_gluedToBase_of_isSeparable

L204 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.quasiSeparated_gluedToBase_of_isSeparable
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
Lean source · statement
theorem quasiSeparated_gluedToBase_of_isSeparable [FiniteDimensional K⟮t⟯ L]
    [Algebra.IsSeparable K⟮t⟯ L] : QuasiSeparated (gluedToBase K t)
theorem

hasLift_generic_of_mem_pullbackVS

L209 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.hasLift_generic_of_mem_pullbackVS
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
Lean source · statement
theorem hasLift_generic_of_mem_pullbackVS [FiniteDimensional K⟮t⟯ L]
    (S : ValuativeCommSq (gluedToBase K t))
    (φ : (glued K t).presheaf.stalk (genericPoint (glued K t)) ⟶ CommRingCat.of S.K)
    (s : L) (i : chartRing K ({s} : Set L) →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
    (hi : ∀ a : chartRing K ({s} : Set L), (i a : L) = a)
    (ιA : Spec (CommRingCat.of (chartRing K ({s} : Set L))) ⟶ glued K t) [IsOpenImmersion ιA]
    [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
    (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk (genericPoint (glued K t)))
    (hs : s ∈ pullbackVS K t S φ) : S.commSq.HasLift
theorem

hasLift_of_generic

L244 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.hasLift_of_generic
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
Lean source · statement
theorem hasLift_of_generic [FiniteDimensional K⟮t⟯ L]
    (S : ValuativeCommSq (gluedToBase K t))
    (hgen : S.i₁.base (IsLocalRing.closedPoint S.K) = genericPoint (glued K t)) :
    S.commSq.HasLift
theorem

gA_mem_range_of_isMaximal

L263 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.gA_mem_range_of_isMaximal
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section Chart
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
include ιA_toBase in
Lean source · statement
theorem gA_mem_range_of_isMaximal [Algebra.FiniteType K A] [IsLocalHom φ.hom]
    [p.asIdeal.IsMaximal]
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk (ιA.base p)) (a : A) :
    gA K t A ιA S p φ a ∈ (algebraMap S.R S.K).range
theorem

mem_range_of_isMaximal

L290 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.mem_range_of_isMaximal
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section Chart
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
include ιA_toBase in
Lean source · statement
theorem mem_range_of_isMaximal [Algebra.FiniteType K A] [IsLocalHom φ.hom]
    [p.asIdeal.IsMaximal]
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk (ιA.base p))
    (x : (glued K t).presheaf.stalk (ιA.base p)) : φ x ∈ (algebraMap S.R S.K).range
theorem

hasLift_closed_of_isMaximal

L322 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.hasLift_closed_of_isMaximal
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
Lean source · statement
theorem hasLift_closed_of_isMaximal (A : Subalgebra K L) [Algebra.FiniteType K A]
    (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
    (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
    (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
    (hp : S.i₁.base (IsLocalRing.closedPoint S.K) = ιA.base p) (hmax : p.asIdeal.IsMaximal) :
    S.commSq.HasLift
theorem

valuativeCriterion_existence_of_isSeparable

L334 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.valuativeCriterion_existence_of_isSeparable
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
Lean source · statement
theorem valuativeCriterion_existence_of_isSeparable [FiniteDimensional K⟮t⟯ L]
    [Algebra.IsSeparable K⟮t⟯ L] : ValuativeCriterion.Existence (gluedToBase K t)
theorem

isProper_gluedToBase_of_isSeparable

L356 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.isProper_gluedToBase_of_isSeparable
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
section Glued
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
Lean source · statement
theorem isProper_gluedToBase_of_isSeparable [FiniteDimensional K⟮t⟯ L]
    [Algebra.IsSeparable K⟮t⟯ L] : IsProper (gluedToBase K t)
instance

isDedekindDomain_chartRing_sm

L383 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.isDedekindDomain_chartRing_sm
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
Lean source · statement
instance isDedekindDomain_chartRing_sm : IsDedekindDomain ↥(chartRing K ({s} : Set
  L))
instance

finite_chartRing_sm

L387 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.finite_chartRing_sm
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
Lean source · statement
instance finite_chartRing_sm :
    Module.Finite ↥(Algebra.adjoin K ({s} : Set L)) ↥(chartRing K ({s} : Set L))
instance

isFractionRing_chartRing_sm

L391 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.isFractionRing_chartRing_sm
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
Lean source · statement
instance isFractionRing_chartRing_sm : IsFractionRing ↥(chartRing K ({s} : Set L)) L
instance

finiteType_chartRing_sm

L395 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.finiteType_chartRing_sm
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
Lean source · statement
instance finiteType_chartRing_sm : Algebra.FiniteType K ↥(chartRing K ({s} : Set L))
instance

chartRing_finitePresentation'

L401 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.chartRing_finitePresentation'
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
Lean source · statement
instance chartRing_finitePresentation' : FinitePresentation K ↥(chartRing K ({s} :
  Set L))
theorem

formallySmooth_chartRing_localization_closed'

L407 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.formallySmooth_chartRing_localization_closed'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem formallySmooth_chartRing_localization_closed' [PerfectField K]
    (𝔪 : Ideal ↥(chartRing K ({s} : Set L))) [𝔪.IsPrime] (h𝔪 : 𝔪 ≠ ⊥) :
    FormallySmooth K (Localization.AtPrime 𝔪)
theorem

formallySmooth_chartRing_localization_bot'

L468 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.formallySmooth_chartRing_localization_bot'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem formallySmooth_chartRing_localization_bot' [PerfectField K] :
    FormallySmooth K (Localization.AtPrime (⊥ : Ideal ↥(chartRing K ({s} : Set L))))
theorem

chartRing_isSmoothAt'

L482 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.chartRing_isSmoothAt'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem chartRing_isSmoothAt' [PerfectField K] (𝔭 : Ideal ↥(chartRing K ({s} : Set L)))
    [𝔭.IsPrime] : IsSmoothAt K 𝔭
theorem

rank_kaehler_eq_one_of_finite_adjoin'

L489 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.rank_kaehler_eq_one_of_finite_adjoin'
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
attribute [local instance] Ideal.Quotient.field
omit [FiniteDimensional ↥K⟮s⟯ L] in
Lean source · statement
theorem rank_kaehler_eq_one_of_finite_adjoin' (hs : Transcendental K s) :
    Module.rank L Ω[L⁄K] = 1
theorem

rank_kaehler_chartRing_localization_away_eq_one'

L496 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.rank_kaehler_chartRing_localization_away_eq_one'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem rank_kaehler_chartRing_localization_away_eq_one' (hs : Transcendental K s)
    (t : chartRing K ({s} : Set L)) (ht : t ≠ 0) :
    Module.rank (Localization.Away t) Ω[(Localization.Away t)⁄K] = 1
theorem

formallySmooth_chartRing'

L519 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.formallySmooth_chartRing'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem formallySmooth_chartRing' [PerfectField K] :
    FormallySmooth K ↥(chartRing K ({s} : Set L))
theorem

locally_isStandardSmoothOfRelativeDimension_one_chartRing'

L524 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.locally_isStandardSmoothOfRelativeDimension_one_chartRing'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem locally_isStandardSmoothOfRelativeDimension_one_chartRing' [PerfectField K]
    (hs : Transcendental K s) :
    RingHom.Locally (RingHom.IsStandardSmoothOfRelativeDimension 1)
      (algebraMap K ↥(chartRing K ({s} : Set L)))
theorem

smoothOfRelativeDimension_one_Spec_chartRing'

L544 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.smoothOfRelativeDimension_one_Spec_chartRing'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem smoothOfRelativeDimension_one_Spec_chartRing' [PerfectField K] (hs : Transcendental
  K s) :
    SmoothOfRelativeDimension 1
      (Spec.map (CommRingCat.ofHom (algebraMap K ↥(chartRing K ({s} : Set L)))))
theorem

smoothOfRelativeDimension_one_gluedToBase'

L553 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7A8SM.smoothOfRelativeDimension_one_gluedToBase'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7A8SM
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.Algebra
open _root_.IntermediateField
open AlgebraicCurve.CurveModel
open scoped AlgebraicCurve.CurveModel
open scoped IntermediateField.algebraAdjoinAdjoin
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
Lean source · statement
theorem smoothOfRelativeDimension_one_gluedToBase' [PerfectField K] (t : L) [Fact (t ≠ 0)]
    (ht : Transcendental K t) [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
    [FiniteDimensional ↥K⟮t⁻¹⟯ L] [Algebra.IsSeparable ↥K⟮t⁻¹⟯ L] :
    SmoothOfRelativeDimension 1 (gluedToBase K t)
instance

isDedekindDomain_chartRing'

L578 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.isDedekindDomain_chartRing'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
open scoped IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
instance isDedekindDomain_chartRing' : IsDedekindDomain ↥(CurveModel.chartRing K
  ({s} : Set L))
instance

finite_chartRing'

L583 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.finite_chartRing'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
open scoped IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
instance finite_chartRing' :
    Module.Finite ↥(Algebra.adjoin K ({s} : Set L)) ↥(CurveModel.chartRing K ({s} : Set L))
instance

isFractionRing_chartRing'

L588 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.isFractionRing_chartRing'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
open scoped IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
instance isFractionRing_chartRing' : IsFractionRing ↥(CurveModel.chartRing K ({s} :
  Set L)) L
instance

finiteType_chartRing'

L592 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.finiteType_chartRing'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
Lean source · statement
instance finiteType_chartRing' : Algebra.FiniteType K ↥(CurveModel.chartRing K ({s}
  : Set L))
instance

isNoetherianRing_chartRing'

L598 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.isNoetherianRing_chartRing'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
Lean source · statement
instance isNoetherianRing_chartRing' : IsNoetherianRing ↥(CurveModel.chartRing K
  ({s} : Set L))
theorem

isMaximal_iff_ne_bot'

L602 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.isMaximal_iff_ne_bot'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
Lean source · statement
theorem isMaximal_iff_ne_bot' (hs : Transcendental K s)
    (𝔭 : Ideal ↥(CurveModel.chartRing K ({s} : Set L))) [𝔭.IsPrime] : 𝔭.IsMaximal ↔ 𝔭 ≠ ⊥
def

primeOfValuationSubring'

L609 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.primeOfValuationSubring'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
variable {K}
Lean source · statement
def primeOfValuationSubring' (O : ValuationSubring L) (hK : ∀ a : K, algebraMap K L a ∈ O)
    (hs : s ∈ O) (hO : O ≠ ⊤) : HeightOneSpectrum ↥(CurveModel.chartRing K ({s} : Set L))
theorem

valuationSubringAtPrime_le'

L613 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.valuationSubringAtPrime_le'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
variable {K}
Lean source · statement
theorem valuationSubringAtPrime_le' (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) (hs : s ∈ O) (hO : O ≠ ⊤) :
    HeightOneSpectrum.valuationSubringAtPrime L (primeOfValuationSubring' s O hK hs hO) ≤ O
theorem

valuationSubringAtPrime_primeOfValuationSubring'

L626 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.valuationSubringAtPrime_primeOfValuationSubring'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
variable {K}
Lean source · statement
theorem valuationSubringAtPrime_primeOfValuationSubring' (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) (hs : s ∈ O) (hO : O ≠ ⊤) :
    HeightOneSpectrum.valuationSubringAtPrime L (primeOfValuationSubring' s O hK hs hO) = O
theorem

exists_ofHeightOneSpectrum_eq'

L631 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.exists_ofHeightOneSpectrum_eq'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
variable {K}
Lean source · statement
theorem exists_ofHeightOneSpectrum_eq' (v : Place K L) (hs : s ∈ v.toValuationSubring) :
    ∃ 𝔭 : HeightOneSpectrum ↥(CurveModel.chartRing K ({s} : Set L)),
      Place.ofHeightOneSpectrum (K := K) 𝔭 = v
theorem

mem_ofHeightOneSpectrum'

L640 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.mem_ofHeightOneSpectrum'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
variable {K}
Lean source · statement
theorem mem_ofHeightOneSpectrum' (𝔭 : HeightOneSpectrum ↥(CurveModel.chartRing K ({s} : Set
  L))) :
    s ∈ (Place.ofHeightOneSpectrum (K := K) (F := L) 𝔭).toValuationSubring
theorem

ofHeightOneSpectrum_injective'

L648 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.ofHeightOneSpectrum_injective'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section OneGenerator
open scoped AlgebraicCurve.CurveModel
variable (s : L) [FiniteDimensional ↥K⟮s⟯ L] [Algebra.IsSeparable ↥K⟮s⟯ L]
variable {K}
Lean source · statement
theorem ofHeightOneSpectrum_injective' :
    Function.Injective
      (Place.ofHeightOneSpectrum (K := K) (F := L) (R := ↥(CurveModel.chartRing K ({s} : Set L))))
instance

locallyOfFiniteType_gluedToBase'

L669 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.locallyOfFiniteType_gluedToBase'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
instance locallyOfFiniteType_gluedToBase' : LocallyOfFiniteType
  (CurveModel.gluedToBase K t)
instance

jacobsonSpace_glued'

L697 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.jacobsonSpace_glued'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
instance jacobsonSpace_glued' : JacobsonSpace (CurveModel.glued K t)
theorem

ι₀_mem_closedPoints_iff'

L700 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.ι₀_mem_closedPoints_iff'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem ι₀_mem_closedPoints_iff' (x : CurveModel.X₀ K t) :
    (CurveModel.ι₀ K t).base x ∈ closedPoints (CurveModel.glued K t) ↔ x ∈ closedPoints
      (CurveModel.X₀ K t)
theorem

ιInf_mem_closedPoints_iff'

L705 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.ιInf_mem_closedPoints_iff'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem ιInf_mem_closedPoints_iff' (x : CurveModel.XInf K t) :
    (CurveModel.ιInf K t).base x ∈ closedPoints (CurveModel.glued K t) ↔
      x ∈ closedPoints (CurveModel.XInf K t)
def

primeOfι₀'

L710 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.primeOfι₀'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
def primeOfι₀' (ht : Transcendental K t) (x₀ : CurveModel.X₀ K t)
    (hx : (CurveModel.ι₀ K t).base x₀ ∈ closedPoints (CurveModel.glued K t)) :
    HeightOneSpectrum ↥(CurveModel.chartRing K ({t} : Set L))
def

primeOfιInf'

L718 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.primeOfιInf'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
def primeOfιInf' (ht : Transcendental K t) (xi : CurveModel.XInf K t)
    (hx : (CurveModel.ιInf K t).base xi ∈ closedPoints (CurveModel.glued K t)) :
    HeightOneSpectrum ↥(CurveModel.chartRing K ({t⁻¹} : Set L))
def

gluedPlaceOfPoint'

L728 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.gluedPlaceOfPoint'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
open scoped Classical in
Lean source · statement
def gluedPlaceOfPoint' (ht : Transcendental K t) (x : closedPoints (CurveModel.glued K t))
  : Place K L
theorem

gluedPlaceOfPoint'_ι₀

L740 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.gluedPlaceOfPoint'_ι₀
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem gluedPlaceOfPoint'_ι₀ (ht : Transcendental K t) (x₀ : CurveModel.X₀ K t)
    (hx : (CurveModel.ι₀ K t).base x₀ ∈ closedPoints (CurveModel.glued K t)) :
    gluedPlaceOfPoint' K t ht ⟨(CurveModel.ι₀ K t).base x₀, hx⟩ =
      Place.ofHeightOneSpectrum (K := K) (primeOfι₀' K t ht x₀ hx)
theorem

gluedPlaceOfPoint'_of_not_mem

L753 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.gluedPlaceOfPoint'_of_not_mem
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · full declaration
theorem gluedPlaceOfPoint'_of_not_mem (ht : Transcendental K t) (x : closedPoints
  (CurveModel.glued K t))
    (h : x.1 ∉ Set.range (CurveModel.ι₀ K t).base) (xi : CurveModel.XInf K t)
    (hxi : (CurveModel.ιInf K t).base xi = x.1) :
    gluedPlaceOfPoint' K t ht x =
      Place.ofHeightOneSpectrum (K := K) (primeOfιInf' K t ht xi (by rw [hxi]; exact x.2)) := by
  have hc : Classical.choose (CurveModel.mem_range_ιInf_of_not_mem_range_ι₀ K t h) = xi :=
    (CurveModel.ιInf K t).isOpenEmbedding.injective
      ((Classical.choose_spec (CurveModel.mem_range_ιInf_of_not_mem_range_ι₀ K t h)).trans hxi.symm)
  have key : ∀ (y : CurveModel.XInf K t) (hy) (_ : y = xi),
      primeOfιInf' K t ht y hy = primeOfιInf' K t ht xi (by rw [hxi]; exact x.2) := by
    rintro y hy rfl; rfl
  unfold gluedPlaceOfPoint'
  rw [dite_eq_right h, key _ _ hc]
theorem

t_mem_of_ι₀'

L768 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.t_mem_of_ι₀'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem t_mem_of_ι₀' (ht : Transcendental K t) (x₀ : CurveModel.X₀ K t) (hx) :
    t ∈ (Place.ofHeightOneSpectrum (K := K) (primeOfι₀' K t ht x₀ hx)).toValuationSubring
theorem

t_not_mem_of_ιInf'

L772 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.t_not_mem_of_ιInf'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem t_not_mem_of_ιInf' (ht : Transcendental K t) (xi : CurveModel.XInf K t) (hx)
    (hxi : CurveModel.tInvChart K t ∈ xi.asIdeal) :
    t ∉ (Place.ofHeightOneSpectrum (K := K) (primeOfιInf' K t ht xi hx)).toValuationSubring
theorem

gluedPlaceOfPoint'_injective

L795 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.gluedPlaceOfPoint'_injective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem gluedPlaceOfPoint'_injective (ht : Transcendental K t) :
    Function.Injective (gluedPlaceOfPoint' K t ht)
theorem

gluedPlaceOfPoint'_surjective

L832 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.gluedPlaceOfPoint'_surjective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem gluedPlaceOfPoint'_surjective (ht : Transcendental K t) :
    Function.Surjective (gluedPlaceOfPoint' K t ht)
theorem

gluedPlaceOfPoint'_bijective

L876 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.gluedPlaceOfPoint'_bijective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem gluedPlaceOfPoint'_bijective (ht : Transcendental K t) :
    Function.Bijective (gluedPlaceOfPoint' K t ht)
theorem

range_stalk_eq_gluedPlaceOfPoint'

L880 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.range_stalk_eq_gluedPlaceOfPoint'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem range_stalk_eq_gluedPlaceOfPoint' (ht : Transcendental K t) (x : closedPoints
  (CurveModel.glued K t)) :
    (((CurveModel.gluedFunctionFieldEquiv K t).symm : (CurveModel.glued K t).functionField ≃+*
      L).toRingHom.comp
        (algebraMap ((CurveModel.glued K t).presheaf.stalk x.1) (CurveModel.glued K
          t).functionField)).range =
      (gluedPlaceOfPoint' K t ht x).toValuationSubring.toSubring
theorem

exists_placeOfPoint_glued

L922 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.exists_placeOfPoint_glued
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
section PlaceDictionary
variable [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L]
Lean source · statement
theorem exists_placeOfPoint_glued (ht : Transcendental K t) :
    ∃ P : closedPoints (CurveModel.glued K t) → Place K L, Function.Bijective P ∧
      ∀ x : closedPoints (CurveModel.glued K t),
        (((CurveModel.gluedFunctionFieldEquiv K t).symm :
              (CurveModel.glued K t).functionField ≃+* L).toRingHom.comp
            (algebraMap ((CurveModel.glued K t).presheaf.stalk x.1)
              (CurveModel.glued K t).functionField)).range =
          (P x).toValuationSubring.toSubring
theorem

finset_subset_affineOpen_glued_of_infinite

L935 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued.S7bP.finset_subset_affineOpen_glued_of_infinite
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
namespace S7bP
section Packaging
open IntermediateField IsDedekindDomain
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
Lean source · statement
theorem finset_subset_affineOpen_glued_of_infinite [Infinite K] [FiniteDimensional ↥K⟮t⟯ L]
  :
    ∀ F : Finset (CurveModel.glued K t), ∃ U : (CurveModel.glued K t).Opens,
      IsAffineOpen U ∧ ∀ x ∈ F, x ∈ U
theorem

isProper_smooth_places_affineCover_glued

L959 ↗
AlgebraicCurve.CurveModel.isProper_smooth_places_affineCover_glued
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isProper_smooth_places_affineCover_glued
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField AlgebraicCurve
  IsLocalRing
open AlgebraicCurve.CurveModel
local instance locallyOfFiniteType_isZariskiLocalAtSource :
    IsZariskiLocalAtSource (@LocallyOfFiniteType) :=
  AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
    (Q := RingHom.FiniteType)
noncomputable section
universe u
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.isProper_smooth_places_affineCover_glued (K : Type u)
  [Field K] [Infinite K]
    [PerfectField K] {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)]
    (ht : Transcendental K t) [FiniteDimensional ↥K⟮t⟯ L] [Algebra.IsSeparable ↥K⟮t⟯ L] :
    IsProper (gluedToBase K t) ∧
    SmoothOfRelativeDimension 1 (gluedToBase K t) ∧
    (∃ P : closedPoints (glued K t) → Place K L, Function.Bijective P ∧
      ∀ x : closedPoints (glued K t),
        (((gluedFunctionFieldEquiv K t).symm : (glued K t).functionField ≃+* L).toRingHom.comp
            (algebraMap ((glued K t).presheaf.stalk x.1) (glued K t).functionField)).range =
          (P x).toValuationSubring.toSubring) ∧
    (∀ F : Finset (glued K t), ∃ U : (glued K t).Opens, IsAffineOpen U ∧ ∀ x ∈ F, x ∈ U)

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