ModulePullbackResidueArtinian.lean
Nyll.SchemeTheory.FiniteEtale.BaseChange.PullbackResidueArtinian
3 declarations indexed from sourceView source ↗ Module documentation
Artinian residue tensors at pullback points
If one projected residue field is finite over the common residue field, its tensor product with the other projected residue field is finite-dimensional over that other field. The categorical tensor in the pullback-carrier API is therefore Artinian as well.
Declarations
AlgebraicGeometry.Scheme.Pullback.leftAlgebra
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits
open scoped TensorProduct
namespace AlgebraicGeometry.Scheme.Pullback
universe u
variable {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
section
variable (T : Triplet f g)
AlgebraicGeometry.Scheme.Pullback.rightAlgebra
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits
open scoped TensorProduct
namespace AlgebraicGeometry.Scheme.Pullback
universe u
variable {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
section
variable (T : Triplet f g)
local instance leftAlgebra :
Algebra (S.residueField T.s) (X.residueField T.x) :=
(((S.residueFieldCongr T.hx).inv ≫
f.residueFieldMap T.x).hom).toAlgebra
AlgebraicGeometry.Scheme.Pullback.Triplet.tensor_isArtinian_of_finiteDimensional_left
DocumentationFiniteness of the left residue-field extension makes the categorical pullback residue tensor Artinian.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits
open scoped TensorProduct
namespace AlgebraicGeometry.Scheme.Pullback
universe u
variable {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
section
variable (T : Triplet f g)
local instance leftAlgebra :
Algebra (S.residueField T.s) (X.residueField T.x) :=
(((S.residueFieldCongr T.hx).inv ≫
f.residueFieldMap T.x).hom).toAlgebra
local instance rightAlgebra :
Algebra (S.residueField T.s) (Y.residueField T.y) :=
(((S.residueFieldCongr T.hy).inv ≫
g.residueFieldMap T.y).hom).toAlgebra