Commit 2023-06-29 18:35 80d2e74b

View on Github →

feat: port AlgebraicGeometry.Pullbacks (#5583)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Pullbacks.lean

added theorem AlgebraicGeometry.Scheme.Pullback.affine_affine_hasPullback

added theorem AlgebraicGeometry.Scheme.Pullback.cocycle

added theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst

added theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd

added theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_snd

added theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst

added theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd

added theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_snd

added def AlgebraicGeometry.Scheme.Pullback.gluedIsLimit

added def AlgebraicGeometry.Scheme.Pullback.gluedLift

added def AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap

added theorem AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst

added theorem AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd

added theorem AlgebraicGeometry.Scheme.Pullback.gluedLift_p1

added theorem AlgebraicGeometry.Scheme.Pullback.gluedLift_p2

added def AlgebraicGeometry.Scheme.Pullback.gluing

added theorem AlgebraicGeometry.Scheme.Pullback.hasPullback_of_cover

added theorem AlgebraicGeometry.Scheme.Pullback.lift_comp_ι

added def AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'

added def AlgebraicGeometry.Scheme.Pullback.openCoverOfBase

added def AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft

added def AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight

added def AlgebraicGeometry.Scheme.Pullback.openCoverOfRight

added def AlgebraicGeometry.Scheme.Pullback.p1

added def AlgebraicGeometry.Scheme.Pullback.p2

added theorem AlgebraicGeometry.Scheme.Pullback.p_comm

added def AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV

added theorem AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst

added theorem AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd

added def AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso

added theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst

added theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd

added theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι

added theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst

added theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd

added def AlgebraicGeometry.Scheme.Pullback.t'

added theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst

added theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd

added theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_snd

added theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst

added theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd

added theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_snd

added def AlgebraicGeometry.Scheme.Pullback.t

added theorem AlgebraicGeometry.Scheme.Pullback.t_fst_fst

added theorem AlgebraicGeometry.Scheme.Pullback.t_fst_snd

added theorem AlgebraicGeometry.Scheme.Pullback.t_id

added theorem AlgebraicGeometry.Scheme.Pullback.t_snd

added def AlgebraicGeometry.Scheme.Pullback.v