Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 16:03 9150268c

View on Github →

feat (algebraic_geometry): Constructions of fibred products of schemes (#11450) This is the first half of the PRs about constructing fibred products of schemes, where we construct all the relevant schemes and morphisms but yet to show that they are actually fibred products.

Estimated changes

Created src/algebraic_geometry/pullbacks.lean

added def algebraic_geometry.Scheme.pullback.V

added theorem algebraic_geometry.Scheme.pullback.cocycle

added theorem algebraic_geometry.Scheme.pullback.cocycle_fst_fst_fst

added theorem algebraic_geometry.Scheme.pullback.cocycle_fst_fst_snd

added theorem algebraic_geometry.Scheme.pullback.cocycle_fst_snd

added theorem algebraic_geometry.Scheme.pullback.cocycle_snd_fst_fst

added theorem algebraic_geometry.Scheme.pullback.cocycle_snd_fst_snd

added theorem algebraic_geometry.Scheme.pullback.cocycle_snd_snd

added def algebraic_geometry.Scheme.pullback.fV

added def algebraic_geometry.Scheme.pullback.glued_lift

added theorem algebraic_geometry.Scheme.pullback.glued_lift_p1

added theorem algebraic_geometry.Scheme.pullback.glued_lift_p2

added def algebraic_geometry.Scheme.pullback.glued_lift_pullback_map

added theorem algebraic_geometry.Scheme.pullback.glued_lift_pullback_map_fst

added theorem algebraic_geometry.Scheme.pullback.glued_lift_pullback_map_snd

added def algebraic_geometry.Scheme.pullback.gluing

added def algebraic_geometry.Scheme.pullback.p1

added def algebraic_geometry.Scheme.pullback.p2

added theorem algebraic_geometry.Scheme.pullback.p_comm

added def algebraic_geometry.Scheme.pullback.t'

added theorem algebraic_geometry.Scheme.pullback.t'_fst_fst_fst

added theorem algebraic_geometry.Scheme.pullback.t'_fst_fst_snd

added theorem algebraic_geometry.Scheme.pullback.t'_fst_snd

added theorem algebraic_geometry.Scheme.pullback.t'_snd_fst_fst

added theorem algebraic_geometry.Scheme.pullback.t'_snd_fst_snd

added theorem algebraic_geometry.Scheme.pullback.t'_snd_snd

added def algebraic_geometry.Scheme.pullback.t

added theorem algebraic_geometry.Scheme.pullback.t_fst_fst

added theorem algebraic_geometry.Scheme.pullback.t_fst_snd

added theorem algebraic_geometry.Scheme.pullback.t_id

added theorem algebraic_geometry.Scheme.pullback.t_snd