Module

isSeparated_sigmaDesc_of_forall_isSeparated.lean

Nyll.AlgebraicCurves.Geometry.Schemes.isSeparated_sigmaDesc_of_forall_isSeparated

1 declaration indexed from sourceView source ↗

Module documentation

is Separated sigma Desc of forall is Separated

Imports10

Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Basic
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Mathlib.CategoryTheory.MorphismProperty.Basic
Mathlib.Tactic.Convert

Imported by2

theorem

isSeparated_sigmaDesc_of_forall_isSeparated

L36 ↗

AlgebraicGeometry.isSeparated_sigmaDesc_of_forall_isSeparated

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isSeparated_sigmaDesc_of_forall_isSeparated
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.isSeparated_sigmaDesc_of_forall_isSeparated
    {σ : Type u} (X : σ → Scheme.{u}) {Y : Scheme.{u}} (f : ∀ i, X i ⟶ Y)
    (hf : ∀ i, IsSeparated (f i)) : IsSeparated (Sigma.desc f)

Module documentation

is Separated sigma Desc of forall is Separated

Declarations

isSeparated_sigmaDesc_of_forall_isSeparated