NYLL
Module

IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
12 declarations indexed from sourceView source ↗

Module documentation

Is Proper exists fg subalgebra of is Proper pullback snd

Imports17
Imported by3

Declarations

abbrev

jY

L62 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.jY
Documentation

The projection from the iterated pullback to the first base-changed scheme.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
abbrev jY
abbrev

σY

L68 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.σY
Documentation

The projection from the iterated pullback to the scheme along which the second pullback is taken.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
abbrev σY
def

ρ

L71 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.ρ
Documentation

The comparison morphism between the iterated pullback and the base-changed target.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
def ρ : pullback (pullback.fst q ι') j ⟶ pullback f ι'
lemma

ρ_fst

L77 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.ρ_fst
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
lemma ρ_fst : ρ f π j q hjq ι' ≫ pullback.fst f ι' = σY j q ι' ≫ π
lemma

ρ_snd

L79 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.ρ_snd
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
lemma ρ_snd : ρ f π j q hjq ι' ≫ pullback.snd f ι' = jY j q ι' ≫ pullback.snd q ι'
lemma

isPullback_ρ

L82 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.isPullback_ρ
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
lemma isPullback_ρ : IsPullback (σY j q ι') (ρ f π j q hjq ι') π (pullback.fst f ι')
instance

surjective_ρ

L90 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.surjective_ρ
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
instance surjective_ρ [Surjective π] : Surjective (ρ f π j q hjq ι')
instance

isProper_ρ

L93 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.isProper_ρ
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
instance isProper_ρ [IsProper π] : IsProper (ρ f π j q hjq ι')
lemma

range_jY

L96 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.range_jY
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
lemma range_jY : Set.range ⇑(jY j q ι') = ⇑(pullback.fst q ι') ⁻¹' Set.range ⇑j
lemma

isClosed_range_jY

L99 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.isClosed_range_jY
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
include hjq in
Lean source · statement
lemma isClosed_range_jY [IsProper π] [IsSeparated q] [IsProper (pullback.snd f ι')] :
    IsClosed (Set.range ⇑(jY j q ι'))
lemma

isProper_snd_of_isClosed_range

L107 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.isProper_snd_of_isClosed_range
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace ProperDesc
section envelope
variable {A₀ : Type u} [CommRing A₀] {X X' P Y : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of A₀)) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A₀))
  (hjq : j ≫ q = π ≫ f) (ι' : Y ⟶ Spec (CommRingCat.of A₀))
include hjq in
Lean source · statement
lemma isProper_snd_of_isClosed_range [IsOpenImmersion j] [IsProper q] [Surjective π] [IsSeparated f]
    [LocallyOfFiniteType f] (h : IsClosed (Set.range ⇑(jY j q ι'))) : IsProper (pullback.snd f ι')
theorem

exists_fg_subalgebra_of_isProper_pullback_snd

L135 ↗
AlgebraicGeometry.IsProper.exists_fg_subalgebra_of_isProper_pullback_snd
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
  AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
  AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
  AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
  AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
  AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-simp] AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
  AlgebraicGeometry.ChowDatum.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
attribute [local instance]
  Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.surjective_ρ
attribute [local instance]
  Schemes.Proofs.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd.ProperDesc.isProper_ρ
open ProperDesc _root_.AlgebraicGeometry.SubalgebraStages in
Lean source · statement
theorem _root_.AlgebraicGeometry.IsProper.exists_fg_subalgebra_of_isProper_pullback_snd
    {A₀ : Type u} [CommRing A₀] [IsNoetherianRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀)) [IsSeparated f] [QuasiCompact f]
      [LocallyOfFiniteType f]
    [IsProper (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))))] (s : Finset A) :
    ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧
      IsProper (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.