ModuleSigmaPullback.lean
Nyll.SchemeTheory.Morphisms.SigmaPullback
3 declarations indexed from sourceView source ↗ Module documentation
Pullback squares for coproducts of schemes
For an arbitrary small family of morphisms, the square formed by a component and the corresponding coproduct inclusions is cartesian. The proof uses the open cover of a coproduct and the equality criterion for points in its components.
Consequently, any property Zariski local on the target holds for the coproduct map exactly when it holds on every component. In particular, a coproduct of finite étale morphisms is finite étale, with no finiteness assumption on the index type.
Imports9
- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
- Mathlib.AlgebraicGeometry.Cover.Open
- Mathlib.AlgebraicGeometry.Limits
- Mathlib.AlgebraicGeometry.Morphisms.Basic
- Mathlib.AlgebraicGeometry.OpenImmersion
- Mathlib.CategoryTheory.Limits.Shapes.Products
- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
- Mathlib.CategoryTheory.MorphismProperty.Basic
- Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Imported by2
Declarations
AlgebraicGeometry.isPullback_sigmaι_sigmaMap
DocumentationA coproduct map restricts to the given morphism on each target component.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u v
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {ι : Type v} [Small.{u} ι] {X Y : ι → Scheme.{u}}
(f : ∀ i, X i ⟶ Y i)
AlgebraicGeometry.IsZariskiLocalAtTarget.sigmaMap_iff
DocumentationProperties local on the target can be checked componentwise on a coproduct map.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u v
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {ι : Type v} [Small.{u} ι] {X Y : ι → Scheme.{u}}
(f : ∀ i, X i ⟶ Y i)
AlgebraicGeometry.IsFiniteEtale.sigmaMap
DocumentationAn arbitrary small coproduct of finite étale morphisms is finite étale.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u v
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {ι : Type v} [Small.{u} ι] {X Y : ι → Scheme.{u}}
(f : ∀ i, X i ⟶ Y i)