Commit 2024-07-11 15:24 8d615693

View on Github →

feat(Limits/Shapes/Pullback): Give pullback.fst and friends explicit parameters (#14526) This PR add changes pullback.fst, pullback.fst, pushout.inr and pushout.inl to have explicit parameters.

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean

modified theorem CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd

modified theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ

modified theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

Modified Mathlib/AlgebraicGeometry/Gluing.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

modified theorem AlgebraicGeometry.Scheme.Pullback.t_fst_fst

modified theorem AlgebraicGeometry.Scheme.Pullback.t_snd

Modified Mathlib/AlgebraicGeometry/Restrict.lean

Modified Mathlib/CategoryTheory/Abelian/Basic.lean

Modified Mathlib/CategoryTheory/Abelian/Pseudoelements.lean

Modified Mathlib/CategoryTheory/Abelian/Refinements.lean

Modified Mathlib/CategoryTheory/Adhesive.lean

Modified Mathlib/CategoryTheory/Adjunction/Over.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/RegularEpi.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/Galois/Basic.lean

Modified Mathlib/CategoryTheory/Galois/Decomposition.lean

Modified Mathlib/CategoryTheory/Generator.lean

Modified Mathlib/CategoryTheory/GlueData.lean

modified theorem CategoryTheory.GlueData.t'_iji

modified theorem CategoryTheory.GlueData.t'_jii

Modified Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean

modified theorem CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr

Modified Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

Modified Mathlib/CategoryTheory/Limits/Over.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

modified def CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit

Modified Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

modified theorem CategoryTheory.Limits.pullback.diagonal_fst

modified theorem CategoryTheory.Limits.pullback.diagonal_isKernelPair

modified theorem CategoryTheory.Limits.pullback.diagonal_snd

Modified Mathlib/CategoryTheory/Limits/Shapes/Images.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean

modified theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom

modified theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv

modified theorem CategoryTheory.Limits.inl_pushoutAssoc_inv

modified theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom

modified theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv

modified theorem CategoryTheory.Limits.inr_pushoutAssoc_hom

modified theorem CategoryTheory.Limits.pullbackAssoc_hom_fst

modified theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst

modified theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd

modified theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst

modified theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd

modified theorem CategoryTheory.Limits.pullbackAssoc_inv_snd

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean

modified theorem CategoryTheory.Limits.fst_eq_snd_of_mono_eq

modified theorem CategoryTheory.Limits.inl_eq_inr_of_epi_eq

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Basic.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean

modified theorem CategoryTheory.regularTopology.mapToEqualizer_eq_comp

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

modified def CategoryTheory.Equalizer.Presieve.Arrows.firstMap

modified def CategoryTheory.Equalizer.Presieve.Arrows.secondMap

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

Modified Mathlib/CategoryTheory/Sites/OneHypercover.lean

modified theorem CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁

Modified Mathlib/CategoryTheory/Sites/Pretopology.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/SmallObject/Construction.lean

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

Modified Mathlib/CategoryTheory/Subobject/Lattice.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

Modified Mathlib/Condensed/TopComparison.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

Modified Mathlib/RingTheory/RingHomProperties.lean

Modified Mathlib/Topology/Category/CompHaus/Limits.lean

Modified Mathlib/Topology/Category/LightProfinite/Limits.lean

Modified Mathlib/Topology/Category/Profinite/Limits.lean

Modified Mathlib/Topology/Category/Stonean/Limits.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

Modified Mathlib/Topology/Gluing.lean