Module

bijective_appTop_of_forall_isMaximal.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_of_forall_isMaximal

8 declarations indexed from sourceView source ↗

Module documentation

bijective app Top of forall is Maximal

Imports5

Mathlib.RingTheory.LocalProperties.Exactness
Mathlib.RingTheory.Localization.BaseChange
Mathlib.Algebra.Category.Ring.Constructions
Mathlib.RingTheory.Flat.Localization
Nyll.AlgebraicCurves.Geometry.Schemes.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat

Imported by2

def

φ

L37 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal.P2LocAux.φ

Documentation

The homomorphism from the base ring to global functions induced by the structure morphism.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace P2LocAux
variable {X : Scheme.{u}} {R : CommRingCat.{u}} (q : X ⟶ Spec R) [CompactSpace X]
  [QuasiSeparatedSpace X]

Lean source · statement

def φ : (R : Type u) →+* (Γ(X, ⊤) : Type u)

abbrev

A

L43 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal.P2LocAux.A

Documentation

The localization of the base ring at the chosen prime ideal.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace P2LocAux
variable {X : Scheme.{u}} {R : CommRingCat.{u}} (q : X ⟶ Spec R) [CompactSpace X]
  [QuasiSeparatedSpace X]
variable (P : Ideal R) [P.IsMaximal]

Lean source · statement

abbrev A : Type u

abbrev

ι

L45 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal.P2LocAux.ι

Documentation

The spectrum morphism induced by localization at the chosen prime ideal.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace P2LocAux
variable {X : Scheme.{u}} {R : CommRingCat.{u}} (q : X ⟶ Spec R) [CompactSpace X]
  [QuasiSeparatedSpace X]
variable (P : Ideal R) [P.IsMaximal]

Lean source · statement

abbrev ι : Spec (CommRingCat.of (A P)) ⟶ Spec R

abbrev

ΓP

L48 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal.P2LocAux.ΓP

Documentation

The ring of global functions on the base change to the local spectrum.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace P2LocAux
variable {X : Scheme.{u}} {R : CommRingCat.{u}} (q : X ⟶ Spec R) [CompactSpace X]
  [QuasiSeparatedSpace X]
variable (P : Ideal R) [P.IsMaximal]

Lean source · statement

abbrev ΓP : Type u

def

ψ

L51 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal.P2LocAux.ψ

Documentation

The structure homomorphism from the local ring to global functions on the base change.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace P2LocAux
variable {X : Scheme.{u}} {R : CommRingCat.{u}} (q : X ⟶ Spec R) [CompactSpace X]
  [QuasiSeparatedSpace X]
variable (P : Ideal R) [P.IsMaximal]

Lean source · statement

def ψ : A P →+* ΓP q P

def

γ

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal.P2LocAux.γ

Documentation

The pullback homomorphism on global functions along the first base-change projection.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace P2LocAux
variable {X : Scheme.{u}} {R : CommRingCat.{u}} (q : X ⟶ Spec R) [CompactSpace X]
  [QuasiSeparatedSpace X]
variable (P : Ideal R) [P.IsMaximal]

Lean source · statement

def γ : (Γ(X, ⊤) : Type u) →+* ΓP q P

theorem

hw

L57 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal.P2LocAux.hw

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace P2LocAux
variable {X : Scheme.{u}} {R : CommRingCat.{u}} (q : X ⟶ Spec R) [CompactSpace X]
  [QuasiSeparatedSpace X]
variable (P : Ideal R) [P.IsMaximal]

Lean source · statement

theorem hw (r : R) : ψ q P (algebraMap R (A P) r) = γ q P (φ q r)

theorem

bijective_appTop_of_forall_isMaximal

L67 ↗

AlgebraicGeometry.bijective_appTop_of_forall_isMaximal

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_forall_isMaximal
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
open P2LocAux in

Lean source · statement

theorem _root_.AlgebraicGeometry.bijective_appTop_of_forall_isMaximal
    {X : Scheme.{u}} {R : CommRingCat.{u}} (q : X ⟶ Spec R) [CompactSpace X] [QuasiSeparatedSpace X]
    (h : ∀ (P : Ideal R) [P.IsMaximal],
      Function.Bijective (pullback.snd q (Spec.map (CommRingCat.ofHom (algebraMap R
        (Localization.AtPrime P))))).appTop) :
    Function.Bijective q.appTop

Module documentation

bijective app Top of forall is Maximal

Declarations