Module

Scheme_quotient_baseChange_of_finiteLocallyFree_of_isPullback.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_quotient_baseChange_of_finiteLocallyFree_of_isPullback

1 declaration indexed from sourceView source ↗

Module documentation

Scheme quotient base Change of finite Locally Free of is Pullback

Imports15

Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.Scheme
Mathlib.AlgebraicGeometry.Sites.Fpqc
Mathlib.CategoryTheory.Category.Basic
Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Mathlib.CategoryTheory.MorphismProperty.Limits

Imported by2

theorem

quotient_baseChange_of_finiteLocallyFree_of_isPullback

L42 ↗

AlgebraicGeometry.Scheme.quotient_baseChange_of_finiteLocallyFree_of_isPullback

Source context 5 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.quotient_baseChange_of_finiteLocallyFree_of_isPullback
    {X R Y X' R' Y' : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}
    [IsFinite p] [Flat p] [LocallyOfFinitePresentation p] [Surjective p]
    (hR : IsPullback s t p p)
    {g : Y' ⟶ Y} {p' : X' ⟶ Y'} {gX : X' ⟶ X} (hX : IsPullback gX p' p g)
    {s' t' : R' ⟶ X'} {gR : R' ⟶ R} (hsq : IsPullback gR s' s gX) (htq : gR ≫ t = t' ≫ gX)
    (w' : s' ≫ p' = t' ≫ p') :
    IsFinite p' ∧ Flat p' ∧ LocallyOfFinitePresentation p' ∧ Surjective p' ∧
      IsPullback s' t' p' p' ∧ Nonempty (IsColimit (Cofork.ofπ p' w'))

Module documentation

Scheme quotient base Change of finite Locally Free of is Pullback

Declarations

quotient_baseChange_of_finiteLocallyFree_of_isPullback