Module

Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite

4 declarations indexed from sourceView source ↗

Module documentation

Scheme Hom quasi Finite At of is Pullback of locally Quasi Finite

Imports1

Nyll.AlgebraicCurves.Geometry.Schemes.LocallyQuasiFinite_descendsAlong_surjective_inf_flat_inf_quasiCompact

Imported by2

theorem

sfq

L33 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite.QFPtDesc.sfq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite
universe u
open CategoryTheory hiding IsDiscrete
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MorphismProperty
open _root_.AlgebraicGeometry
namespace QFPtDesc

Lean source · statement

theorem sfq {X Y : Scheme.{u}} (q : X ⟶ Y) (x : X) :
    (@Surjective ⊓ @Flat ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) (Spec.map
      (q.residueFieldMap x))

theorem

locallyQuasiFinite_fiberToSpecResidueField

L42 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite.QFPtDesc.locallyQuasiFinite_fiberToSpecResidueField

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite
universe u
open CategoryTheory hiding IsDiscrete
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MorphismProperty
open _root_.AlgebraicGeometry
namespace QFPtDesc

Lean source · statement

theorem locallyQuasiFinite_fiberToSpecResidueField
    {X Y X' Y' : Scheme.{u}} {f : X ⟶ Y} {f' : X' ⟶ Y'} {p : X' ⟶ X} {q : Y' ⟶ Y}
    (sq : IsPullback p f' f q) [LocallyQuasiFinite f'] (y' : Y') :
    LocallyQuasiFinite (f.fiberToSpecResidueField (q y'))

theorem

main

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite.QFPtDesc.main

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite
universe u
open CategoryTheory hiding IsDiscrete
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MorphismProperty
open _root_.AlgebraicGeometry
namespace QFPtDesc

Lean source · statement

theorem main
    {X Y X' Y' : Scheme.{u}} {f : X ⟶ Y} {f' : X' ⟶ Y'} {p : X' ⟶ X} {q : Y' ⟶ Y}
    (sq : IsPullback p f' f q) [LocallyOfFiniteType f] [LocallyQuasiFinite f'] (y' : Y') (x : X)
    (hx : f x = q y') : f.QuasiFiniteAt x

theorem

quasiFiniteAt_of_isPullback_of_locallyQuasiFinite

L75 ↗

AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_of_isPullback_of_locallyQuasiFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite
universe u
open CategoryTheory hiding IsDiscrete
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MorphismProperty
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_of_isPullback_of_locallyQuasiFinite
    {X Y X' Y' : Scheme.{u}} {f : X ⟶ Y} {f' : X' ⟶ Y'} {p : X' ⟶ X} {q : Y' ⟶ Y}
    (sq : IsPullback p f' f q) [LocallyOfFiniteType f] [LocallyQuasiFinite f'] (y' : Y') (x : X)
    (hx : f x = q y') : f.QuasiFiniteAt x

Module documentation

Scheme Hom quasi Finite At of is Pullback of locally Quasi Finite

Declarations

sfq

locallyQuasiFinite_fiberToSpecResidueField

main

quasiFiniteAt_of_isPullback_of_locallyQuasiFinite