ModuleRawOverlapFiniteness.lean
Nyll.SchemeTheory.FiniteEtale.RawOverlapFiniteness
5 declarations indexed from sourceView source ↗ Module documentation
Actual finiteness hypotheses for raw overlap Hom descent
The local models are finite etale over affine charts. Their raw overlaps are open subschemes of affine models, and are compact because the original base is quasi-separated. Their ambient maps are locally finitely presented. No overlap is claimed finite over the whole ambient base.
Declarations
AlgebraicGeometry.Scheme.Cover.rawLocalModel_isAffine
DocumentationEvery actual local covering scheme is affine.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S : Scheme.{u}} (𝒰 : S.OpenCover)
(M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
[∀ i : 𝒰.I₀, IsAffine (𝒰.X i)]
[∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
AlgebraicGeometry.Scheme.Cover.rawOverlap_compactSpace
DocumentationRaw overlaps are compact over a quasi-separated ambient base.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S : Scheme.{u}} (𝒰 : S.OpenCover)
(M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
[∀ i : 𝒰.I₀, IsAffine (𝒰.X i)]
[∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
AlgebraicGeometry.Scheme.Cover.rawOverlap_quasiCompact
DocumentationThe raw overlap ambient morphism is quasi-compact.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S : Scheme.{u}} (𝒰 : S.OpenCover)
(M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
[∀ i : 𝒰.I₀, IsAffine (𝒰.X i)]
[∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
AlgebraicGeometry.Scheme.Cover.rawOverlap_quasiSeparated
DocumentationA raw overlap is an open subscheme of an affine local model, so its ambient structural map is quasi-separated.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S : Scheme.{u}} (𝒰 : S.OpenCover)
(M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
[∀ i : 𝒰.I₀, IsAffine (𝒰.X i)]
[∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
AlgebraicGeometry.Scheme.Cover.rawOverlap_locallyOfFinitePresentation
DocumentationThe raw overlap ambient map is locally finitely presented: it is an open immersion followed by a finite-etale map and an open chart map.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S : Scheme.{u}} (𝒰 : S.OpenCover)
(M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
[∀ i : 𝒰.I₀, IsAffine (𝒰.X i)]
[∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
omit [∀ i : 𝒰.I₀, IsAffine (𝒰.X i)] in