Module

LocallyQuasiFinite_descendsAlong_surjective_inf_flat_inf_quasiCompact.lean

Nyll.AlgebraicCurves.Geometry.Schemes.LocallyQuasiFinite_descendsAlong_surjective_inf_flat_inf_quasiCompact

2 declarations indexed from sourceView source ↗

Module documentation

Locally Quasi Finite descends Along surjective inf flat inf quasi Compact

Imports4

Mathlib.AlgebraicGeometry.Morphisms.Descent
Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Mathlib.AlgebraicGeometry.Morphisms.Flat
Nyll.AlgebraicCurves.Foundations.Algebra.RingHom_QuasiFinite_codescendsAlong_faithfullyFlat

Imported by2

theorem

descendsAlong_surjective_inf_flat_inf_quasiCompact'

L41 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.LocallyQuasiFinite_descendsAlong_surjective_inf_flat_inf_quasiCompact.AlgebraicGeometry.LocallyQuasiFinite.descendsAlong_surjective_inf_flat_inf_quasiCompact'

Documentation

Local quasi-finiteness descends along a surjective, flat, quasi-compact morphism.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace LocallyQuasiFinite_descendsAlong_surjective_inf_flat_inf_quasiCompact
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MorphismProperty
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry _root_.AlgebraicGeometry.LocallyQuasiFinite in

Lean source · statement

theorem AlgebraicGeometry.LocallyQuasiFinite.descendsAlong_surjective_inf_flat_inf_quasiCompact' :
    DescendsAlong (@LocallyQuasiFinite : MorphismProperty Scheme.{u}) (@Surjective ⊓ @Flat ⊓
      @QuasiCompact)

theorem

descendsAlong_surjective_inf_flat_inf_quasiCompact

L113 ↗

AlgebraicGeometry.LocallyQuasiFinite.descendsAlong_surjective_inf_flat_inf_quasiCompact