Mathlib Changelog
v3
Changelog
About
Github
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