ModuleFlatBaseChangeAffinization.lean
Nyll.SchemeTheory.Affine.FlatBaseChangeAffinization
2 declarations indexed from sourceView source ↗ Module documentation
Affinization commutes with flat affine base change
The qcqs theorem on sections gives an actual pushout square of global sections. Applying Spec and cancelling the affine base square proves that the canonical affinization map commutes with the given base change.
Imports3
- Mathlib.AlgebraicGeometry.Morphisms.Flat
- Mathlib.AlgebraicGeometry.Pullbacks
- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Imported by9
Declarations
AlgebraicGeometry.isPushout_appTop_of_flat
DocumentationThe actual maps on global sections form a pushout after flat affine base change of a qcqs morphism.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
variable {X S T : Scheme.{u}} (f : X ⟶ S) (g : T ⟶ S)
variable [IsAffine S] [IsAffine T] [QuasiCompact f] [QuasiSeparated f] [Flat g]
AlgebraicGeometry.isPullback_toSpecΓ_of_flat
DocumentationThe canonical affinization morphism is compatible with flat affine base change, as an actual cartesian square.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
variable {X S T : Scheme.{u}} (f : X ⟶ S) (g : T ⟶ S)
variable [IsAffine S] [IsAffine T] [QuasiCompact f] [QuasiSeparated f] [Flat g]