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