Commit 2022-01-31 20:42 a0bb6ea9

View on Github →

feat(algebraic_geometry): Open covers of the fibred product. (#11733)

Estimated changes

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.Scheme.open_cover.copy

added def algebraic_geometry.Scheme.open_cover.pushforward_iso

added def algebraic_geometry.Scheme.open_cover_of_is_iso

Modified src/algebraic_geometry/pullbacks.lean

added def algebraic_geometry.Scheme.pullback.open_cover_of_base'

added def algebraic_geometry.Scheme.pullback.open_cover_of_base

added def algebraic_geometry.Scheme.pullback.open_cover_of_left

added def algebraic_geometry.Scheme.pullback.open_cover_of_right