Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 08:38 bf347f9c

View on Github →

feat(algebraic_geometry): Fiber products of schemes (#10605)

Estimated changes

Modified src/algebraic_geometry/gluing.lean

added theorem algebraic_geometry.Scheme.open_cover.hom_ext

Modified src/algebraic_geometry/pullbacks.lean

added theorem algebraic_geometry.Scheme.pullback.affine_affine_has_pullback

added def algebraic_geometry.Scheme.pullback.glued_is_limit

added theorem algebraic_geometry.Scheme.pullback.has_pullback_of_cover

added theorem algebraic_geometry.Scheme.pullback.lift_comp_ι

added def algebraic_geometry.Scheme.pullback.pullback_fst_ι_to_V

added theorem algebraic_geometry.Scheme.pullback.pullback_fst_ι_to_V_fst

added theorem algebraic_geometry.Scheme.pullback.pullback_fst_ι_to_V_snd

added def algebraic_geometry.Scheme.pullback.pullback_p1_iso

added theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_hom_fst

added theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_hom_snd

added theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_hom_ι

added theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_inv_fst

added theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_inv_snd