NYLL
Module

exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
15 declarations indexed from sourceView source ↗

Module documentation

exists is Proper surjective is Open Immersion comp eq of is Separated

Imports14
Imported by2

Declarations

lemma

coprodMap_of

L54 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.coprodMap_of
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Coprod
Lean source · statement
lemma coprodMap_of {P : MorphismProperty Scheme.{u}} [IsZariskiLocalAtTarget P]
    {X Y X' Y' : Scheme.{u}} (a : X ⟶ X') (b : Y ⟶ Y') (ha : P a) (hb : P b) :
    P (coprod.map a b)
instance

isOpenImmersion_coprodMap

L68 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.isOpenImmersion_coprodMap
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Coprod
Lean source · statement
instance isOpenImmersion_coprodMap {X Y X' Y' : Scheme.{u}} (a : X ⟶ X') (b : Y ⟶ Y')
    [IsOpenImmersion a] [IsOpenImmersion b] : IsOpenImmersion (coprod.map a b)
instance

isProper_coprodMap

L72 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.isProper_coprodMap
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Coprod
Lean source · statement
instance isProper_coprodMap {X Y X' Y' : Scheme.{u}} (a : X ⟶ X') (b : Y ⟶ Y')
    [IsProper a] [IsProper b] : IsProper (coprod.map a b)
instance

isProper_coprodDesc

L76 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.isProper_coprodDesc
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Coprod
Lean source · statement
instance isProper_coprodDesc {U V X : Scheme.{u}} (a : U ⟶ X) (b : V ⟶ X)
    [IsProper a] [IsProper b] : IsProper (coprod.desc a b)
lemma

range_coprodDesc

L83 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.range_coprodDesc
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Coprod
Lean source · statement
lemma range_coprodDesc {U V X : Scheme.{u}} (a : U ⟶ X) (b : V ⟶ X) :
    Set.range (coprod.desc a b) = Set.range a ∪ Set.range b
def

HasEnvelope

L106 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.HasEnvelope
Documentation

A subset admits a proper envelope that embeds openly in a scheme proper over the base.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Envelope
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
Lean source · statement
def HasEnvelope (S : Set X) : Prop
lemma

empty

L110 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.HasEnvelope.empty
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Envelope
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
Lean source · statement
lemma HasEnvelope.empty : HasEnvelope f ∅
lemma

union

L123 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.HasEnvelope.union
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Envelope
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
variable {f}
Lean source · statement
lemma HasEnvelope.union {S T : Set X} (hS : HasEnvelope f S) (hT : HasEnvelope f T) :
    HasEnvelope f (S ∪ T)
lemma

of_isIntegral

L136 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.HasEnvelope.of_isIntegral
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Envelope
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
variable {f}
variable (f)
Lean source · statement
lemma HasEnvelope.of_isIntegral [IsNoetherianRing A] [IsSeparated f] [LocallyOfFiniteType f]
    [QuasiCompact f] {Z : Scheme.{u}} [IsIntegral Z] (i : Z ⟶ X) [IsClosedImmersion i] :
    HasEnvelope f (Set.range i)
lemma

isReduced_subscheme_vanishingIdeal

L150 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.isReduced_subscheme_vanishingIdeal
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Reduced
variable {X : Scheme.{u}}
Lean source · statement
lemma isReduced_subscheme_vanishingIdeal (Z : Closeds X) :
    IsReduced (Scheme.IdealSheafData.vanishingIdeal Z).subscheme
lemma

isIntegral_subscheme_vanishingIdeal

L156 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.isIntegral_subscheme_vanishingIdeal
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Reduced
variable {X : Scheme.{u}}
Lean source · statement
lemma isIntegral_subscheme_vanishingIdeal (Z : Closeds X) (hZ : IsIrreducible (Z : Set X)) :
    IsIntegral (Scheme.IdealSheafData.vanishingIdeal Z).subscheme
lemma

hasEnvelope_of_mem_irreducibleComponents

L173 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.hasEnvelope_of_mem_irreducibleComponents
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Main
variable {A : Type u} [CommRing A] [IsNoetherianRing A]
  {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
  [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
Lean source · statement
lemma hasEnvelope_of_mem_irreducibleComponents (Z : Set X) (hZ : Z ∈ irreducibleComponents X) :
    HasEnvelope f Z
lemma

hasEnvelope_biUnion

L181 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.hasEnvelope_biUnion
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Main
variable {A : Type u} [CommRing A] [IsNoetherianRing A]
  {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
  [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
Lean source · statement
lemma hasEnvelope_biUnion (s : Finset (Set X)) (hs : ↑s ⊆ irreducibleComponents X) :
    HasEnvelope f (⋃ Z ∈ s, Z)
theorem

main

L192 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.main
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
namespace SolCH
section Main
variable {A : Type u} [CommRing A] [IsNoetherianRing A]
  {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
  [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
Lean source · statement
theorem main :
    ∃ (X' P : Scheme.{u}) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A)),
      IsProper π ∧ Surjective π ∧ IsOpenImmersion j ∧ IsProper q ∧ j ≫ q = π ≫ f
theorem

exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated

L223 ↗
AlgebraicGeometry.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
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 TopologicalSpace Topology
universe u
attribute [local instance]
  exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.isOpenImmersion_coprodMap
attribute [local instance]
  Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.isProper_coprodMap
attribute [local instance]
  Proofs.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated.SolCH.isProper_coprodDesc
Lean source · statement
theorem _root_.AlgebraicGeometry.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] :
    ∃ (X' P : Scheme.{u}) (π : X' ⟶ X) (j : X' ⟶ P) (q : P ⟶ Spec (CommRingCat.of A)),
      IsProper π ∧ Surjective π ∧ IsOpenImmersion j ∧ IsProper q ∧ j ≫ q = π ≫ f

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