Commit 2024-08-02 19:53 9756867d

View on Github →

feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts (#14428)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Gluing.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

added def AlgebraicGeometry.coprodIsoSigma

added def AlgebraicGeometry.coprodMk

added theorem AlgebraicGeometry.coprodMk_inl

added theorem AlgebraicGeometry.coprodMk_inr

added def AlgebraicGeometry.coprodOpenCover.{w}

added def AlgebraicGeometry.coprodSpec

added theorem AlgebraicGeometry.coprodSpec_apply

added theorem AlgebraicGeometry.coprodSpec_coprodMk

added theorem AlgebraicGeometry.coprodSpec_inl

added theorem AlgebraicGeometry.coprodSpec_inr

added theorem AlgebraicGeometry.isCompl_opensRange_inl_inr

added theorem AlgebraicGeometry.isCompl_range_inl_inr

added theorem AlgebraicGeometry.isIso_stalkMap_coprodSpec

added def AlgebraicGeometry.sigmaSpec

added theorem AlgebraicGeometry.ι_left_coprodIsoSigma_inv

added theorem AlgebraicGeometry.ι_right_coprodIsoSigma_inv

added theorem AlgebraicGeometry.ι_sigmaSpec

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.of_isLocalization

deleted theorem AlgebraicGeometry.Scheme.IsOpenImmersion.of_isLocalization

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

added theorem CategoryTheory.Limits.fst_opProdIsoCoprod_hom

added theorem CategoryTheory.Limits.inl_opProdIsoCoprod_inv

added theorem CategoryTheory.Limits.inr_opProdIsoCoprod_inv

added def CategoryTheory.Limits.opProdIsoCoprod

added theorem CategoryTheory.Limits.opProdIsoCoprod_hom_fst

added theorem CategoryTheory.Limits.opProdIsoCoprod_hom_snd

added theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inl

added theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inr

added theorem CategoryTheory.Limits.snd_opProdIsoCoprod_hom