Module

LocallyQuasiFinite_of_flat_of_locallyQuasiFinite_genericFiber.lean

Nyll.AlgebraicCurves.Geometry.Schemes.LocallyQuasiFinite_of_flat_of_locallyQuasiFinite_genericFiber

1 declaration indexed from sourceView source ↗

Module documentation

Locally Quasi Finite of flat of locally Quasi Finite generic Fiber

Imports9

Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Mathlib.RingTheory.RingHom.QuasiFinite
Mathlib.Tactic.Algebraize
Mathlib.Tactic.ClearExclamation
Mathlib.Tactic.WLOG
Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_QuasiFinite_of_flat_of_quasiFinite_genericFiber

Imported by2

theorem

of_flat_of_locallyQuasiFinite_genericFiber

L36 ↗

AlgebraicGeometry.LocallyQuasiFinite.of_flat_of_locallyQuasiFinite_genericFiber

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace LocallyQuasiFinite_of_flat_of_locallyQuasiFinite_genericFiber
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.LocallyQuasiFinite.of_flat_of_locallyQuasiFinite_genericFiber
    {R K : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [Ring.DimensionLEOne R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    {Y : Scheme.{u}} (f : Y ⟶ Spec (.of R)) [Flat f] [LocallyOfFiniteType f]
    [LocallyQuasiFinite (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R K))))] :
    LocallyQuasiFinite f

Module documentation

Locally Quasi Finite of flat of locally Quasi Finite generic Fiber

Declarations

of_flat_of_locallyQuasiFinite_genericFiber