NYLL
Module

bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
22 declarations indexed from sourceView source ↗

Module documentation

bijective app Top of is Proper of flat of is Noetherian Ring of is Local Ring

Imports22
Imported by2

Declarations

lemma

bijective_of_isPushout_of_faithfullyFlat

L53 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.bijective_of_isPushout_of_faithfullyFlat
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
Lean source · statement
lemma bijective_of_isPushout_of_faithfullyFlat {R S B P : CommRingCat.{u}} {f : R ⟶ S} {g : R ⟶ B}
    {inl : S ⟶ P} {inr : B ⟶ P} (H : IsPushout f g inl inr)
    (hg : g.hom.FaithfullyFlat)
    (hinr : Function.Bijective inr) : Function.Bijective f
abbrev

Ahat

L91 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.Ahat
Documentation

The completion of the local ring with respect to its maximal ideal.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section Completion
variable (A : CommRingCat.{u}) [IsNoetherianRing A] [IsLocalRing A]
Lean source · statement
abbrev Ahat : Type u
instance

(anonymous instance)

L93 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section Completion
variable (A : CommRingCat.{u}) [IsNoetherianRing A] [IsLocalRing A]
Lean source · statement
instance : IsNoetherianRing (Ahat A)
instance

(anonymous instance)

L95 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section Completion
variable (A : CommRingCat.{u}) [IsNoetherianRing A] [IsLocalRing A]
Lean source · statement
instance : IsAdicComplete (IsLocalRing.maximalIdeal (Ahat A)) (Ahat A)
instance

(anonymous instance)

L100 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section Completion
variable (A : CommRingCat.{u}) [IsNoetherianRing A] [IsLocalRing A]
Lean source · statement
instance : Module.FaithfullyFlat A (Ahat A)
def

resMap

L112 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.resMap
Documentation

The induced homomorphism from the residue field to the residue field of the completion.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section Completion
variable (A : CommRingCat.{u}) [IsNoetherianRing A] [IsLocalRing A]
Lean source · statement
def resMap : A ⧸ IsLocalRing.maximalIdeal A →+* Ahat A ⧸ IsLocalRing.maximalIdeal (Ahat A)
lemma

resMap_bijective

L116 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.resMap_bijective
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section Completion
variable (A : CommRingCat.{u}) [IsNoetherianRing A] [IsLocalRing A]
Lean source · statement
lemma resMap_bijective : Function.Bijective (resMap A)
def

resIso

L136 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.resIso
Documentation

The isomorphism identifying the residue field with that of the completed local ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section Completion
variable (A : CommRingCat.{u}) [IsNoetherianRing A] [IsLocalRing A]
Lean source · statement
def resIso : CommRingCat.of (A ⧸ IsLocalRing.maximalIdeal A) ≅
    CommRingCat.of (Ahat A ⧸ IsLocalRing.maximalIdeal (Ahat A))
lemma

quot_comp_resIso

L140 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.quot_comp_resIso
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section Completion
variable (A : CommRingCat.{u}) [IsNoetherianRing A] [IsLocalRing A]
Lean source · statement
lemma quot_comp_resIso :
    CommRingCat.ofHom (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) ≫ (resIso A).hom =
      CommRingCat.ofHom (algebraMap A (Ahat A)) ≫
        CommRingCat.ofHom (Ideal.Quotient.mk (IsLocalRing.maximalIdeal (Ahat A)))
lemma

appTop_bijective_of_isIso

L148 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.appTop_bijective_of_isIso
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
Lean source · statement
lemma appTop_bijective_of_isIso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] :
    Function.Bijective f.appTop
lemma

appLE_top_top'

L152 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.appLE_top_top'
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
Lean source · statement
lemma appLE_top_top' {Y Z : Scheme.{u}} (f : Y ⟶ Z) : f.appLE ⊤ ⊤ le_top = f.appTop
abbrev

jA

L161 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.jA
Documentation

The spectrum morphism induced by the map into the adic completion.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
Lean source · statement
abbrev jA : Spec (CommRingCat.of (Ahat A)) ⟶ Spec A
abbrev

Xh

L165 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.Xh
Documentation

The base change of the scheme to the completed local ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
Lean source · statement
abbrev Xh : Scheme.{u}
abbrev

ph

L168 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.ph
Documentation

The structure morphism of the base change to the completed local ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
Lean source · statement
abbrev ph : Xh p ⟶ Spec (CommRingCat.of (Ahat A))
abbrev

gh

L171 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.gh
Documentation

The projection from the completed base change to the original scheme.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
Lean source · statement
abbrev gh : Xh p ⟶ X
instance

(anonymous instance)

L173 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
Lean source · statement
instance : IsProper (ph p)
instance

(anonymous instance)

L175 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
Lean source · statement
instance : Flat (jA (A := A))
lemma

closedFibre_bijective

L182 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.closedFibre_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
omit [IsProper p] [Flat p] in
Lean source · statement
lemma closedFibre_bijective
    (h : Function.Bijective (pullback.snd p (Spec.map (CommRingCat.ofHom
      (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))))).appTop) :
    Function.Bijective (pullback.snd (ph p) (Spec.map (CommRingCat.ofHom
      (Ideal.Quotient.mk (IsLocalRing.maximalIdeal (Ahat A)))))).appTop
lemma

isPushout_appTop

L220 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.isPushout_appTop
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
omit [Flat p] in
Lean source · statement
lemma isPushout_appTop :
    IsPushout p.appTop (jA (A := A)).appTop (gh p).appTop (ph p).appTop
lemma

jA_appTop_faithfullyFlat

L234 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.jA_appTop_faithfullyFlat
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
Lean source · statement
lemma jA_appTop_faithfullyFlat : (jA (A := A)).appTop.hom.FaithfullyFlat
theorem

main

L247 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing.SolH0Nloc.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
noncomputable section
namespace SolH0Nloc
section BaseChange
variable {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
  (p : X ⟶ Spec A) [IsProper p] [Flat p]
Lean source · statement
theorem main
    (h : Function.Bijective (pullback.snd p (Spec.map (CommRingCat.ofHom
      (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))))).appTop) :
    Function.Bijective p.appTop
theorem

bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing

L299 ↗
AlgebraicGeometry.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace TensorProduct
universe u
Lean source · statement
theorem
  _root_.AlgebraicGeometry.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
    {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
    (p : X ⟶ Spec A) [IsProper p] [Flat p]
    (h : Function.Bijective (pullback.snd p (Spec.map (CommRingCat.ofHom
      (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))))).appTop) :
    Function.Bijective p.appTop

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