Module

bijective_appTop_of_isProper_of_flat_of_isAdicComplete.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_of_isProper_of_flat_of_isAdicComplete

61 declarations indexed from sourceView source ↗

Module documentation

bijective app Top of is Proper of flat of is Adic Complete

Imports25

Mathlib.Algebra.Category.Ring.Constructions
Mathlib.Algebra.Ring.Subring.Basic
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.LinearAlgebra.TensorProduct.Quotient
Mathlib.LinearAlgebra.SModEq.Basic
Mathlib.RingTheory.AdicCompletion.Basic
Mathlib.RingTheory.Filtration
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Ideal.Colon
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.RingHom.Flat
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Mathlib.Topology.Sheaves.Stalks
Mathlib.Tactic.Algebraize
Mathlib.Tactic.Choose
Mathlib.Tactic.Push
Mathlib.Tactic.Ring.RingNF

Imported by2

lemma

mem_map_colon_of_flat

L54 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T1.mem_map_colon_of_flat

Source context 6 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace SolH0T1

Lean source · statement

lemma mem_map_colon_of_flat {A C : Type*} [CommRing A] [CommRing C] (f : A →+* C)
    (hf : f.Flat) (I : Ideal A) (π : A) (c : C) (h : f π * c ∈ I.map f) :
    c ∈ (I.colon {π}).map f

lemma

ker_eq_map_and_surjective_of_isPushout

L94 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T1.ker_eq_map_and_surjective_of_isPushout

Source context 6 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace SolH0T1

Lean source · statement

lemma ker_eq_map_and_surjective_of_isPushout {R A B P : CommRingCat} {f : R ⟶ A} {g : R ⟶ B}
    {inl : A ⟶ P} {inr : B ⟶ P} (H : IsPushout f g inl inr)
    (hg : Function.Surjective g) :
    RingHom.ker inl.hom = Ideal.map f.hom (RingHom.ker g.hom) ∧ Function.Surjective inl

abbrev

quot

L155 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.quot

Documentation

The quotient map by an ideal, regarded as a morphism of commutative rings.

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

abbrev quot (I : Ideal A) : A ⟶ CommRingCat.of (A ⧸ I)

abbrev

XI

L158 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.XI

Documentation

The closed base change of the scheme to the quotient by an ideal.

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

abbrev XI (I : Ideal A) : Scheme.{u}

abbrev

ι

L161 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.ι

Documentation

The first projection from the closed base change to the original scheme.

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

abbrev ι (I : Ideal A) : XI p I ⟶ X

abbrev

pI

L164 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.pI

Documentation

The structure morphism from the closed base change to the quotient spectrum.

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

abbrev pI (I : Ideal A) : XI p I ⟶ Spec (.of (A ⧸ I))

def

alg

L166 ↗

SolH0T2.alg

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

def _root_.SolH0T2.alg (U : X.Opens) : A →+* Γ(X, U)

def

φ

L172 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.φ

Documentation

The homomorphism from the quotient ring to global functions on the closed base change.

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

def φ (I : Ideal A) : A ⧸ I →+* Γ(XI p I, ⊤)

lemma

alg_map

L175 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.alg_map

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma alg_map {U V : X.Opens} (i : V ≤ U) (a : A) :
    X.presheaf.map (homOfLE i).op (alg p U a) = alg p V a

lemma

appLE_top_top

L182 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.appLE_top_top

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma appLE_top_top {Y Z : Scheme.{u}} (f : Y ⟶ Z) :
    f.appLE ⊤ ⊤ le_top = f.appTop

lemma

appLE_congr_hom

L186 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.appLE_congr_hom

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma appLE_congr_hom {Y Z : Scheme.{u}} {f g : Y ⟶ Z} (h : f = g) (U : Z.Opens) (V : Y.Opens)
    (e : V ≤ f ⁻¹ᵁ U) (e' : V ≤ g ⁻¹ᵁ U) : f.appLE U V e = g.appLE U V e'

lemma

ker_ι_app

L190 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.ker_ι_app

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma ker_ι_app (I : Ideal A) {U : X.Opens} (hU : IsAffineOpen U) :
    RingHom.ker ((ι p I).app U).hom = I.map (alg p U) ∧ Function.Surjective ((ι p I).app U)

def

LiftsAt

L243 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt

Documentation

A local section lifts the restriction of a global section on the closed base change.

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

def LiftsAt (I : Ideal A) (U : X.Opens) (t : Γ(XI p I, ⊤)) (c : Γ(X, U)) : Prop

lemma

exists

L246 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.exists

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.exists (I : Ideal A) {U : X.Opens} (hU : IsAffineOpen U) (t : Γ(XI p I, ⊤)) :
    ∃ c, LiftsAt p I U t c

lemma

zero

L250 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.zero

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.zero (I : Ideal A) (U : X.Opens) : LiftsAt p I U 0 0

lemma

add

L253 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.add

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.add {I : Ideal A} {U : X.Opens} {t t' : Γ(XI p I, ⊤)} {c c' : Γ(X, U)}
    (h : LiftsAt p I U t c) (h' : LiftsAt p I U t' c') : LiftsAt p I U (t + t') (c + c')

lemma

sub

L257 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.sub

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.sub {I : Ideal A} {U : X.Opens} {t t' : Γ(XI p I, ⊤)} {c c' : Γ(X, U)}
    (h : LiftsAt p I U t c) (h' : LiftsAt p I U t' c') : LiftsAt p I U (t - t') (c - c')

lemma

mul

L261 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.mul

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.mul {I : Ideal A} {U : X.Opens} {t t' : Γ(XI p I, ⊤)} {c c' : Γ(X, U)}
    (h : LiftsAt p I U t c) (h' : LiftsAt p I U t' c') : LiftsAt p I U (t * t') (c * c')

lemma

sub_mem_iff

L265 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.sub_mem_iff

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.sub_mem_iff {I : Ideal A} {U : X.Opens} (hU : IsAffineOpen U) {t : Γ(XI p I, ⊤)}
    {c c' : Γ(X, U)} (h : LiftsAt p I U t c) :
    LiftsAt p I U t c' ↔ c - c' ∈ I.map (alg p U)

lemma

mem_iff_of_zero

L273 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.mem_iff_of_zero

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.mem_iff_of_zero {I : Ideal A} {U : X.Opens} (hU : IsAffineOpen U) {c : Γ(X, U)} :
    LiftsAt p I U 0 c ↔ c ∈ I.map (alg p U)

lemma

restrict

L279 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.restrict

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.restrict {I : Ideal A} {U V : X.Opens} (i : V ≤ U) {t : Γ(XI p I, ⊤)} {c : Γ(X, U)}
    (h : LiftsAt p I U t c) : LiftsAt p I V t (X.presheaf.map (homOfLE i).op c)

lemma

alg

L290 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.alg

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.alg (I : Ideal A) (U : X.Opens) (a : A) :
    LiftsAt p I U (φ p I (Ideal.Quotient.mk I a)) (alg p U a)

lemma

eq_zero_of_forall_affine

L323 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.eq_zero_of_forall_affine

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma eq_zero_of_forall_affine (I : Ideal A) (t : Γ(XI p I, ⊤))
    (h : ∀ U : X.affineOpens, (XI p I).presheaf.map (homOfLE (le_top (a := (ι p I) ⁻¹ᵁ U))).op t =
      0) :
    t = 0

lemma

eq_zero_of_forall_liftsAt

L337 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.eq_zero_of_forall_liftsAt

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma eq_zero_of_forall_liftsAt (I : Ideal A) (t : Γ(XI p I, ⊤))
    (h : ∀ U : X.affineOpens, ∀ c, LiftsAt p I U t c → c ∈ I.map (alg p U)) : t = 0

lemma

eq_of_forall_liftsAt

L348 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.eq_of_forall_liftsAt

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma eq_of_forall_liftsAt (I : Ideal A) (t t' : Γ(XI p I, ⊤))
    (h : ∀ U : X.affineOpens, ∃ c, LiftsAt p I U t c ∧ LiftsAt p I U t' c) : t = t'

lemma

quot_comp_factor

L368 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.quot_comp_factor

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma quot_comp_factor {I J : Ideal A} (h : I ≤ J) :
    quot I ≫ CommRingCat.ofHom (Ideal.Quotient.factor h) = quot (A := A) J

def

τ

L373 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.τ

Documentation

The transition morphism between closed base changes induced by an inclusion of ideals.

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

def τ {I J : Ideal A} (h : I ≤ J) : XI p J ⟶ XI p I

lemma

τ_ι

L377 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.τ_ι

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma τ_ι {I J : Ideal A} (h : I ≤ J) : τ p h ≫ ι p I = ι p J

lemma

τ_pI

L380 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.τ_pI

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma τ_pI {I J : Ideal A} (h : I ≤ J) :
    τ p h ≫ pI p I = pI p J ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor h))

def

ρ

L385 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.ρ

Documentation

The transition homomorphism on global sections induced by an inclusion of ideals.

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

def ρ {I J : Ideal A} (h : I ≤ J) : Γ(XI p I, ⊤) →+* Γ(XI p J, ⊤)

lemma

presheaf_map_congr

L387 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.presheaf_map_congr

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma presheaf_map_congr {Y : Scheme.{u}} {U V : Y.Opens} (i j : op U ⟶ op V) (s : Γ(Y, U)) :
    Y.presheaf.map i s = Y.presheaf.map j s

lemma

trans

L391 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LiftsAt.trans

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LiftsAt.trans {I J : Ideal A} (hIJ : I ≤ J) {U : X.Opens} {t : Γ(XI p I, ⊤)} {c : Γ(X, U)}
    (h : LiftsAt p I U t c) : LiftsAt p J U (ρ p hIJ t) c

lemma

ρ_φ

L407 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.ρ_φ

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma ρ_φ {I J : Ideal A} (hIJ : I ≤ J) (a : A) :
    ρ p hIJ (φ p I (Ideal.Quotient.mk I a)) = φ p J (Ideal.Quotient.mk J a)

def

LocData

L414 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LocData

Documentation

A local lift together with a divisibility relation modulo the chosen ideal.

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

def LocData (I : Ideal A) (π : A) (t : Γ(XI p I, ⊤)) (U : X.affineOpens) (c d : Γ(X, U)) : Prop

lemma

restrict

L417 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.LocData.restrict

Source context 8 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)

Lean source · statement

lemma LocData.restrict {I : Ideal A} {π : A} {t : Γ(XI p I, ⊤)} {U W : X.affineOpens}
    (i : (W : X.Opens) ≤ U)
    {c d : Γ(X, U)} (h : LocData p I π t U c d) :
    LocData p I π t W (X.presheaf.map (homOfLE i).op c) (X.presheaf.map (homOfLE i).op d)

structure

StepHyp

L439 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp

Documentation

The flatness, ideal, and section-bijectivity hypotheses for one induction step through a small ideal extension.

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)

Lean source · full declaration

structure StepHyp : Prop where
  /-- The structure homomorphism on each affine chart is flat. -/
  flat : ∀ U : X.affineOpens, (alg p U).Flat
  /-- The chosen element belongs to the maximal ideal. -/
  hπm : π ∈ 𝔪
  /-- The chosen element is not in the smaller ideal. -/
  hπI : π ∉ I
  /-- Multiplication by the chosen element sends the maximal ideal into the smaller ideal. -/
  hmul : ∀ a ∈ 𝔪, a * π ∈ I
  /-- The smaller ideal is contained in the maximal ideal. -/
  hIm : I ≤ 𝔪
  /-- The map on global sections is bijective over the maximal-ideal quotient. -/
  bijm : Function.Bijective (φ p 𝔪)
  /-- The map on global sections is bijective after adjoining the chosen element to the ideal. -/
  bijI' : Function.Bijective (φ p (I ⊔ Ideal.span {π}))

lemma

le_sup

L458 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.le_sup

Source context 14 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S
omit [𝔪.IsMaximal] S in

Lean source · statement

lemma StepHyp.le_sup : I ≤ I ⊔ Ideal.span {π}

lemma

colon_eq

L460 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.colon_eq

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

lemma StepHyp.colon_eq : I.colon {π} = 𝔪

lemma

span_mul_le

L469 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.span_mul_le

Source context 14 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S
omit [𝔪.IsMaximal] in

Lean source · statement

lemma StepHyp.span_mul_le : Ideal.span {π} * 𝔪 ≤ I

lemma

pi_mul_mem

L474 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.pi_mul_mem

Source context 14 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S
omit [𝔪.IsMaximal] in

Lean source · statement

lemma StepHyp.pi_mul_mem {U : X.affineOpens} {x : Γ(X, U)} (hx : x ∈ 𝔪.map (alg p U)) :
    alg p U π * x ∈ I.map (alg p U)

lemma

exists_locData

L481 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.exists_locData

Source context 14 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S
omit [𝔪.IsMaximal] S in

Lean source · statement

lemma StepHyp.exists_locData {t : Γ(XI p I, ⊤)} (ht : ρ p (le_sup_left : I ≤ I ⊔ Ideal.span {π}) t
  = 0) (U : X.affineOpens) :
    ∃ c d, LocData p I π t U c d

lemma

locData_unique

L496 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.locData_unique

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

lemma StepHyp.locData_unique {t : Γ(XI p I, ⊤)} {U : X.affineOpens} {c d c' d' : Γ(X, U)}
    (h : LocData p I π t U c d) (h' : LocData p I π t U c' d') :
    d - d' ∈ 𝔪.map (alg p U)

def

eLoc

L508 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.eLoc

Documentation

The local section over the maximal-ideal fibre obtained from the chosen divisibility witness.

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

def StepHyp.eLoc {t : Γ(XI p I, ⊤)} (ht : ρ p (le_sup_left : I ≤ I ⊔ Ideal.span {π}) t = 0) (U :
  X.affineOpens) :
    Γ(XI p 𝔪, (ι p 𝔪) ⁻¹ᵁ U)

lemma

eLoc_eq

L513 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.eLoc_eq

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

lemma StepHyp.eLoc_eq {t : Γ(XI p I, ⊤)} (ht : ρ p (le_sup_left : I ≤ I ⊔ Ideal.span {π}) t = 0) (U
  : X.affineOpens)
    {c d : Γ(X, U)} (h : LocData p I π t U c d) :
    StepHyp.eLoc (p := p) (𝔪 := 𝔪) (I := I) (π := π) ht U = (ι p 𝔪).app U d

lemma

eLoc_restrict

L522 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.eLoc_restrict

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

lemma StepHyp.eLoc_restrict {t : Γ(XI p I, ⊤)} (ht : ρ p (le_sup_left : I ≤ I ⊔ Ideal.span {π}) t =
  0) {U W : X.affineOpens}
    (i : (W : X.Opens) ≤ U) :
    (XI p 𝔪).presheaf.map (homOfLE ((ι p 𝔪).preimage_mono i)).op
      (StepHyp.eLoc (p := p) (𝔪 := 𝔪) (I := I) (π := π) ht U) =
        StepHyp.eLoc (p := p) (𝔪 := 𝔪) (I := I) (π := π) ht W

lemma

exists_glue

L539 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.exists_glue

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

lemma StepHyp.exists_glue {t : Γ(XI p I, ⊤)} (ht : ρ p (le_sup_left : I ≤ I ⊔ Ideal.span {π}) t =
  0) :
    ∃ g : Γ(XI p 𝔪, ⊤), ∀ U : X.affineOpens,
      (XI p 𝔪).presheaf.map (homOfLE le_top).op g =
        StepHyp.eLoc (p := p) (𝔪 := 𝔪) (I := I) (π := π) ht U

lemma

ker_ρ

L577 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.ker_ρ

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

lemma StepHyp.ker_ρ {t : Γ(XI p I, ⊤)} (ht : ρ p (le_sup_left : I ≤ I ⊔ Ideal.span {π}) t = 0) :
    ∃ u : A, t = φ p I (Ideal.Quotient.mk I (u * π))

lemma

injective

L603 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.injective

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

lemma StepHyp.injective : Function.Injective (φ p I)

lemma

surjective

L638 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.surjective

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

lemma StepHyp.surjective : Function.Surjective (φ p I)

lemma

bijective

L648 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.StepHyp.bijective

Source context 13 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
section Step
variable {p}
variable (𝔪 : Ideal A) [𝔪.IsMaximal] (I : Ideal A) (π : A)
variable {𝔪 I π} (S : StepHyp (p := p) 𝔪 I π)
include S

Lean source · statement

lemma StepHyp.bijective : Function.Bijective (φ p I)

lemma

alg_flat

L672 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.alg_flat

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)

Lean source · statement

lemma alg_flat [Flat p] (U : X.affineOpens) : (alg p U).Flat

theorem

levels_bijective

L677 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.levels_bijective

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)

Lean source · statement

theorem levels_bijective [IsNoetherianRing A] [IsLocalRing A] [Flat p]
    (hm : Function.Bijective (φ p 𝔪)) :
    ∀ I : Ideal A, I ≤ 𝔪 → (∃ k, 𝔪 ^ k ≤ I) → Function.Bijective (φ p I)

lemma

map_top_apply

L727 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.map_top_apply

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)

Lean source · statement

lemma map_top_apply (I : Ideal A) (t : Γ(XI p I, ⊤)) :
    (XI p I).presheaf.map (homOfLE (le_top (a := (ι p I) ⁻¹ᵁ ⊤))).op t = t

lemma

ι_appTop_alg

L732 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.ι_appTop_alg

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)

Lean source · statement

lemma ι_appTop_alg (I : Ideal A) (a : A) :
    (ι p I).appTop (alg p ⊤ a) = φ p I (Ideal.Quotient.mk I a)

lemma

res_mem_of_ι_appTop_eq_zero

L739 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.res_mem_of_ι_appTop_eq_zero

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)

Lean source · statement

lemma res_mem_of_ι_appTop_eq_zero (I : Ideal A) (t : Γ(X, ⊤)) (ht : (ι p I).appTop t = 0)
    (U : X.affineOpens) : X.presheaf.map (homOfLE le_top).op t ∈ I.map (alg p U)

theorem

eq_zero_of_forall_ι_appTop_eq_zero

L750 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.eq_zero_of_forall_ι_appTop_eq_zero

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)

Lean source · statement

theorem eq_zero_of_forall_ι_appTop_eq_zero [IsNoetherianRing A] [IsLocalRing A] [IsProper p]
    (t : Γ(X, ⊤)) (ht : ∀ k : ℕ, (ι p (𝔪 ^ (k + 1))).appTop t = 0) : t = 0

lemma

smodEq_pow_iff

L827 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.smodEq_pow_iff

Source context 12 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)
omit p in

Lean source · statement

lemma smodEq_pow_iff [IsLocalRing A] {x y : A} {n : ℕ} :
    x ≡ y [SMOD (𝔪 ^ n • ⊤ : Submodule A A)] ↔ x - y ∈ 𝔪 ^ n

theorem

bijective_alg_top

L831 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.bijective_alg_top

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)

Lean source · statement

theorem bijective_alg_top [IsNoetherianRing A] [IsLocalRing A] [IsAdicComplete 𝔪 A]
    [IsProper p] [Flat p] (hm : Function.Bijective (φ p 𝔪)) :
    Function.Bijective (alg p ⊤)

lemma

bijective_φ_iff

L889 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.bijective_φ_iff

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)

Lean source · statement

lemma bijective_φ_iff (I : Ideal A) :
    Function.Bijective (φ p I) ↔ Function.Bijective ((pI p I).appTop)

theorem

bijective_appTop

L896 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_isAdicComplete.SolH0T2.bijective_appTop

Source context 11 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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
noncomputable section
namespace SolH0T2
variable {X : Scheme.{u}} {A : CommRingCat.{u}} (p : X ⟶ Spec A)
local notation "𝔪" => IsLocalRing.maximalIdeal (CommRingCat.carrier A)

Lean source · statement

theorem bijective_appTop [IsNoetherianRing A] [IsLocalRing A] [IsAdicComplete 𝔪 A]
    [IsProper p] [Flat p] (h : Function.Bijective ((pI p 𝔪).appTop)) :
    Function.Bijective p.appTop

theorem

bijective_appTop_of_isProper_of_flat_of_isAdicComplete

L918 ↗

AlgebraicGeometry.bijective_appTop_of_isProper_of_flat_of_isAdicComplete

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_isAdicComplete
open CategoryTheory CategoryTheory.Limits TensorProduct AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI
attribute [local simp] SolH0T2.τ_ι
attribute [local simp] SolH0T2.τ_pI

Lean source · statement

theorem _root_.AlgebraicGeometry.bijective_appTop_of_isProper_of_flat_of_isAdicComplete
    {X : Scheme.{u}} {A : CommRingCat.{u}} [IsNoetherianRing A] [IsLocalRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) 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

Module documentation

bijective app Top of is Proper of flat of is Adic Complete

Declarations