Module

isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.lean

Nyll.AlgebraicCurves.Geometry.Schemes.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat

45 declarations indexed from sourceView source ↗

Module documentation

is Pushout app Top pullback fst app Top pullback snd of flat

Imports8

Mathlib.Algebra.Category.Ring.Constructions
Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.AlgebraicGeometry.Over
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.LinearAlgebra.TensorProduct.Pi
Mathlib.RingTheory.Flat.Basic
Mathlib.Topology.QuasiSeparated
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Imported by5

abbrev

bc

L43 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.bc

Documentation

The spectrum morphism induced by the scalar extension from k to A.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

abbrev bc : Spec (CommRingCat.of A) ⟶ Spec (CommRingCat.of k)

def

toSec

L47 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.toSec

Documentation

The base ring homomorphism into sections on an open of the scheme over Spec k.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

def toSec (U : X.Opens) : CommRingCat.of k ⟶ Γ(X, U)

theorem

appLE_top_top

L51 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.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 isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

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

theorem

toSec_top

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.toSec_top

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem toSec_top : toSec fX ⊤ = (Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fX.appTop

theorem

toSec_map

L58 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.toSec_map

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem toSec_map {U V : X.Opens} (i : Opposite.op U ⟶ Opposite.op V) :
    toSec fX U ≫ X.presheaf.map i = toSec fX V

abbrev

toSecA

L64 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.toSecA

Documentation

The scalar homomorphism into sections on the inverse image after base change.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

abbrev toSecA (U : X.Opens) :
    CommRingCat.of A ⟶ Γ(pullback fX (bc A), (pullback.fst fX (bc A)) ⁻¹ᵁ U)

theorem

appLE_congrHom

L68 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.appLE_congrHom

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem appLE_congrHom {Y : Scheme.{u}} {f g : X ⟶ Y} (h : f = g) (U : Y.Opens) (V : X.Opens)
    (e : V ≤ f ⁻¹ᵁ U) : f.appLE U V e = g.appLE U V (h ▸ e)

theorem

toSec_app

L72 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.toSec_app

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem toSec_app (U : X.Opens) :
    toSec fX U ≫ (pullback.fst fX (bc A)).app U =
      CommRingCat.ofHom (algebraMap k A) ≫ toSecA fX A U

theorem

isPushout_toSec_app

L79 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.isPushout_toSec_app

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem isPushout_toSec_app {U : X.Opens} (hU : IsAffineOpen U) :
    IsPushout (CommRingCat.ofHom (algebraMap k A)) (toSec fX U) (toSecA fX A U)
      ((pullback.fst fX (bc A)).app U)

instance

secAlgebra

L131 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.secAlgebra

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]

Lean source · statement

instance secAlgebra (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))] (U : X.Opens) :
    Algebra k Γ(X, U)

theorem

algebraMap_sec

L135 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.algebraMap_sec

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]

Lean source · statement

theorem algebraMap_sec (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))] (U : X.Opens) :
    algebraMap k Γ(X, U) = (toSec (X ↘ Spec (CommRingCat.of k)) U).hom

def

resAlgHom

L141 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.resAlgHom

Documentation

Restriction of sections as an algebra homomorphism over the base ring.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]

Lean source · statement

def resAlgHom {U V : X.Opens} (h : V ≤ U) : Γ(X, U) →ₐ[k] Γ(X, V)

theorem

resAlgHom_apply

L148 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.resAlgHom_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]

Lean source · statement

theorem resAlgHom_apply {U V : X.Opens} (h : V ≤ U) (s : Γ(X, U)) :
    resAlgHom k X h s = X.presheaf.map (homOfLE h).op s

abbrev

res

L152 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.res

Documentation

Restriction of sections as a linear map over the base ring.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]

Lean source · statement

abbrev res {U V : X.Opens} (h : V ≤ U) : Γ(X, U) →ₗ[k] Γ(X, V)

theorem

res_apply

L154 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.res_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]

Lean source · statement

theorem res_apply {U V : X.Opens} (h : V ≤ U) (s : Γ(X, U)) :
    res k X h s = X.presheaf.map (homOfLE h).op s

abbrev

XA

L160 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.XA

Documentation

The scheme obtained by extending the scalars of X from k to A.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

abbrev XA : Scheme.{u}

abbrev

fstA

L163 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.fstA

Documentation

The projection from the scalar extension back to X.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

abbrev fstA : XA k X A ⟶ X

instance

secAlgebraK

L169 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.secAlgebraK

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

instance secAlgebraK (W : (XA k X A).Opens) : Algebra k Γ(XA k X A, W)

instance

isScalarTower_secK

L172 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.isScalarTower_secK

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

instance isScalarTower_secK (W : (XA k X A).Opens) : IsScalarTower k A Γ(XA k X A, W)

def

appAlgHom

L176 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.appAlgHom

Documentation

Pullback of sections along the base change projection, as a base algebra homomorphism.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

def appAlgHom (V : X.Opens) : Γ(X, V) →ₐ[k] Γ(XA k X A, (fstA k X A) ⁻¹ᵁ V)

theorem

appAlgHom_apply

L183 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.appAlgHom_apply

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem appAlgHom_apply (V : X.Opens) (s : Γ(X, V)) :
    appAlgHom k X A V s = (fstA k X A).app V s

instance

appAlgebra

L186 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.appAlgebra

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

instance appAlgebra (V : X.Opens) : Algebra Γ(X, V) Γ(XA k X A, (fstA k X A) ⁻¹ᵁ V)

instance

isScalarTower_app

L189 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.isScalarTower_app

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

instance isScalarTower_app (V : X.Opens) : IsScalarTower k Γ(X, V) Γ(XA k X A, (fstA k X A)
  ⁻¹ᵁ V)

def

baseChangeSections

L194 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.baseChangeSections

Documentation

The canonical map from the tensor product to sections after base change.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

def baseChangeSections (V : X.Opens) : A ⊗[k] Γ(X, V) →ₐ[A] Γ(XA k X A, (fstA k X A) ⁻¹ᵁ V)

theorem

baseChangeSections_tmul

L197 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.baseChangeSections_tmul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem baseChangeSections_tmul (V : X.Opens) (a : A) (s : Γ(X, V)) :
    baseChangeSections k X A V (a ⊗ₜ s) = algebraMap A _ a * (fstA k X A).app V s

theorem

preimage_mono

L201 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.preimage_mono

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem preimage_mono {U V : X.Opens} (h : V ≤ U) : (fstA k X A) ⁻¹ᵁ V ≤ (fstA k X A) ⁻¹ᵁ U

theorem

res_baseChangeSections

L204 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.res_baseChangeSections

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem res_baseChangeSections {U V : X.Opens} (h : V ≤ U) (x : A ⊗[k] Γ(X, U)) :
    res A (XA k X A) (preimage_mono k X A h) (baseChangeSections k X A U x) =
      baseChangeSections k X A V (LinearMap.lTensor A (res k X h) x)

theorem

isPushout_sections

L217 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.isPushout_sections

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem isPushout_sections {U : X.Opens} (hU : IsAffineOpen U) :
    Algebra.IsPushout k A Γ(X, U) Γ(XA k X A, (fstA k X A) ⁻¹ᵁ U)

theorem

baseChangeSections_eq_equiv

L221 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.baseChangeSections_eq_equiv

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · full declaration

theorem baseChangeSections_eq_equiv {U : X.Opens} (hU : IsAffineOpen U) :
    haveI := isPushout_sections k X A hU
    (baseChangeSections k X A U : A ⊗[k] Γ(X, U) → _) =
      Algebra.IsPushout.equiv k A Γ(X, U) (Γ(XA k X A, (fstA k X A) ⁻¹ᵁ U)) := by
  have := isPushout_sections k X A hU
  have : baseChangeSections k X A U = (Algebra.IsPushout.equiv k A Γ(X, U)
      Γ(XA k X A, (fstA k X A) ⁻¹ᵁ U)).toAlgHom := by
    apply Algebra.TensorProduct.ext'
    intro a s
    rw [baseChangeSections_tmul]
    change _ = Algebra.IsPushout.equiv k A Γ(X, U) Γ(XA k X A, (fstA k X A) ⁻¹ᵁ U) (a ⊗ₜ s)
    rw [Algebra.IsPushout.equiv_tmul]
    rfl
  exact congrArg (fun f : _ →ₐ[A] _ => (f : A ⊗[k] Γ(X, U) → _)) this

theorem

bijective_baseChangeSections

L236 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.bijective_baseChangeSections

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
section Over
variable (k : Type u) [CommRing k]
variable (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
variable (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem bijective_baseChangeSections {U : X.Opens} (hU : IsAffineOpen U) :
    Function.Bijective (baseChangeSections k X A U)

theorem

sections_ext

L256 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.sections_ext

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Sheaf
variable {Y : Scheme.{u}} {ι : Type u} (W : ι → Y.Opens) (V : Y.Opens) (hle : ∀ i, W i ≤ V) (hV : V
  ≤ iSup W)
include hV in

Lean source · statement

theorem sections_ext (s t : Γ(Y, V)) (h : ∀ i, Y.presheaf.map (homOfLE (hle i)).op s =
  Y.presheaf.map (homOfLE (hle i)).op t) :
    s = t

theorem

sections_glue

L261 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.sections_glue

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Sheaf
variable {Y : Scheme.{u}} {ι : Type u} (W : ι → Y.Opens) (V : Y.Opens) (hle : ∀ i, W i ≤ V) (hV : V
  ≤ iSup W)
include hV in

Lean source · statement

theorem sections_glue (p : ∀ i, Γ(Y, W i))
    (hp : ∀ i j, Y.presheaf.map (homOfLE inf_le_left).op (p i) = Y.presheaf.map (homOfLE
      inf_le_right).op (p j)) :
    ∃ s : Γ(Y, V), ∀ i, Y.presheaf.map (homOfLE (hle i)).op s = p i

theorem

bijective_of_flat_of_exact

L272 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.bijective_of_flat_of_exact

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite

Lean source · statement

theorem bijective_of_flat_of_exact
    {k : Type u} [CommRing k] {A : Type u} [CommRing A] [Algebra k A] [Module.Flat k A]
    {M P Q : Type u} [AddCommGroup M] [AddCommGroup P] [AddCommGroup Q] [Module k M] [Module k P]
      [Module k Q]
    {M' P' Q' : Type u} [AddCommGroup M'] [AddCommGroup P'] [AddCommGroup Q']
    [Module k M'] [Module k P'] [Module k Q']
    (ρ : M →ₗ[k] P) (δ : P →ₗ[k] Q) (hρ : Function.Injective ρ) (hex : Function.Exact ρ δ)
    (ρ' : M' →ₗ[k] P') (δ' : P' →ₗ[k] Q') (hρ' : Function.Injective ρ') (hex' : Function.Exact ρ'
      δ')
    (α : A ⊗[k] M →ₗ[k] M') (β : A ⊗[k] P →ₗ[k] P') (γ : A ⊗[k] Q →ₗ[k] Q')
    (hαβ : β ∘ₗ (ρ.lTensor A) = ρ' ∘ₗ α) (hβγ : γ ∘ₗ (δ.lTensor A) = δ' ∘ₗ β)
    (hβ : Function.Bijective β) (hγ : Function.Injective γ) :
    Function.Bijective α

abbrev

resPi

L310 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.resPi

Documentation

Simultaneous restriction of a section to a family of opens.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Cech
variable (k : Type u) [CommRing k] (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

abbrev resPi {ι : Type u} {V : X.Opens} (W : ι → X.Opens) (hle : ∀ i, W i ≤ V) :
    Γ(X, V) →ₗ[k] (∀ i, Γ(X, W i))

theorem

injective_resPi

L314 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.injective_resPi

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Cech
variable (k : Type u) [CommRing k] (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem injective_resPi {ι : Type u} {V : X.Opens} (W : ι → X.Opens) (hle : ∀ i, W i ≤ V) (hV : V ≤
  iSup W) :
    Function.Injective (resPi k X W hle)

theorem

piRight_lTensor_resPi

L322 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.piRight_lTensor_resPi

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Cech
variable (k : Type u) [CommRing k] (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · full declaration

theorem piRight_lTensor_resPi {ι : Type u} [Fintype ι] [DecidableEq ι] {V : X.Opens} (W : ι →
  X.Opens)
    (hle : ∀ i, W i ≤ V) (x : A ⊗[k] Γ(X, V)) (i : ι) :
    TensorProduct.piRight k k A (fun i => Γ(X, W i)) (LinearMap.lTensor A (resPi k X W hle) x) i =
      LinearMap.lTensor A (res k X (hle i)) x := by
  induction x using TensorProduct.inductionOn with
  | add x y hx hy => simp only [map_add, Pi.add_apply, hx, hy]
  | tmul a s => simp [TensorProduct.piRight_apply]

theorem

injective_baseChangeSections

L331 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.injective_baseChangeSections

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Cech
variable (k : Type u) [CommRing k] (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem injective_baseChangeSections [Module.Flat k A] {V : X.Opens} (hV : IsCompact (V : Set X)) :
    Function.Injective (baseChangeSections k X A V)

theorem

res_res

L359 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.res_res

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Cech
variable (k : Type u) [CommRing k] (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem res_res {U V W : X.Opens} (h₁ : V ≤ U) (h₂ : W ≤ V) (s : Γ(X, U)) :
    res k X h₂ (res k X h₁ s) = res k X (h₂.trans h₁) s

theorem

exists_finite_affine_cover

L365 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.exists_finite_affine_cover

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Cech
variable (k : Type u) [CommRing k] (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem exists_finite_affine_cover {V : X.Opens} (hV : IsCompact (V : Set X)) :
    ∃ (ι : Type u) (_ : Fintype ι) (W : ι → X.Opens), (∀ i, IsAffineOpen (W i)) ∧ (∀ i, W i ≤ V) ∧
      V ≤ iSup W

abbrev

cechDiff

L383 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.cechDiff

Documentation

The difference of the two restriction maps on pairwise intersections.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Cech
variable (k : Type u) [CommRing k] (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

abbrev cechDiff {ι : Type u} (U : ι → X.Opens) :
    (∀ i, Γ(X, U i)) →ₗ[k] (∀ ij : ι × ι, Γ(X, U ij.1 ⊓ U ij.2))

theorem

exact_resPi_cechDiff

L388 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.exact_resPi_cechDiff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Cech
variable (k : Type u) [CommRing k] (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem exact_resPi_cechDiff {ι : Type u} {V : X.Opens} (U : ι → X.Opens) (hle : ∀ i, U i ≤ V) (hV
  : V ≤ iSup U) :
    Function.Exact (resPi k X U hle) (cechDiff k X U)

theorem

bijective_baseChangeSections_top

L404 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.bijective_baseChangeSections_top

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Cech
variable (k : Type u) [CommRing k] (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))]
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem bijective_baseChangeSections_top [CompactSpace X] [QuasiSeparatedSpace X] [Module.Flat k A]
  :
    Function.Bijective (baseChangeSections k X A ⊤)

theorem

isPushout_appTop

L492 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.isPushout_appTop

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Final
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem isPushout_appTop [CompactSpace X] [QuasiSeparatedSpace X] [Module.Flat k A] :
    IsPushout (CommRingCat.ofHom (algebraMap k A))
      ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fX.appTop)
      ((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
        (pullback.snd fX (Spec.map (CommRingCat.ofHom (algebraMap k A)))).appTop)
      (pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap k A)))).appTop

theorem

bijective_appTop_snd

L524 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat.FBC0.bijective_appTop_snd

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
noncomputable section
namespace FBC0
open TopologicalSpace Opposite
section Final
variable {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
  (A : Type u) [CommRing A] [Algebra k A]

Lean source · statement

theorem bijective_appTop_snd {k : Type u} [Field k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of
  k))
    [CompactSpace X] [QuasiSeparatedSpace X]
    (hX : Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fX.appTop).hom)
    (A : Type u) [CommRing A] [Algebra k A] :
    Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
      (pullback.snd fX (Spec.map (CommRingCat.ofHom (algebraMap k A)))).appTop).hom

theorem

isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat

L547 ↗

AlgebraicGeometry.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct in

Lean source · statement

theorem _root_.AlgebraicGeometry.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
    {k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
    [CompactSpace X] [QuasiSeparatedSpace X]
    (A : Type u) [CommRing A] [Algebra k A] [Module.Flat k A] :
    IsPushout (CommRingCat.ofHom (algebraMap k A))
      ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fX.appTop)
      ((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
        (pullback.snd fX (Spec.map (CommRingCat.ofHom (algebraMap k A)))).appTop)
      (pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap k A)))).appTop

Module documentation

is Pushout app Top pullback fst app Top pullback snd of flat

Declarations