Merge master into nightly-testing

Author: mathlib-nightly-testing[bot]

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: b6def9edd1c39de8602b8c177c66e9416e5dbc60
+    default: 8c3d31d2beba80d86de30b6ccd373d2c3a76b26e
   path:
     description: Checkout destination path.
     required: false

Mathlib.lean

@@ -1510,6 +1510,7 @@ public import Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
 public import Mathlib.AlgebraicTopology.SimplicialObject.II
 public import Mathlib.AlgebraicTopology.SimplicialObject.Op
 public import Mathlib.AlgebraicTopology.SimplicialObject.Split
+public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
@@ -3638,6 +3639,7 @@ public import Mathlib.Condensed.Light.InternallyProjective
 public import Mathlib.Condensed.Light.Limits
 public import Mathlib.Condensed.Light.Module
 public import Mathlib.Condensed.Light.Monoidal
+public import Mathlib.Condensed.Light.Sequence
 public import Mathlib.Condensed.Light.Small
 public import Mathlib.Condensed.Light.TopCatAdjunction
 public import Mathlib.Condensed.Light.TopComparison

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Basic.lean

@@ -0,0 +1,166 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
+public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
+public import Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
+public import Mathlib.AlgebraicTopology.SimplicialSet.Presentable
+public import Mathlib.CategoryTheory.SmallObject.Basic
+
+/-!
+# Anodyne extensions
+
+Anodyne extensions form a property of morphisms in the category of simplicial
+sets. It contains horn inclusions and it is closed under coproducts, pushouts,
+transfinite compositions and retracts. Equivalently, using the small
+object argument, anodyne extensions can be defined (and are defined here)
+as the class of morphisms that satisfy the left lifting property with respect
+to the class of fibrations (for the Quillen model category structure:
+fibrations are morphisms that have the right lifting property with respect
+to horn inclusions). When the Quillen model category structure is fully
+upstreamed (TODO @joelriou), it can be shown that a morphism `f` is an
+anodyne extension iff `f` is a cofibration that is also a weak equivalence.
+
+We also introduce the class of strong anodyne extensions that could be defined
+as a closure similarly as anodyne extensions, but without taking the closure
+under retracts. Sean Moss has given a combinatorial description of these
+strong anodyne extensions: the inclusion `A.ι : A ⟶ X` of a subcomplex `A`
+of a simplicial set `X` is a strong anodyne extension iff there exists
+a regular pairing for `A`. In this file, we define strong anodyne extensions
+in terms of such regular pairings, and using the main result of the file
+`Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean`
+we show that a strong anodyne extension is an anodyne extension.
+
+## TODO
+* introduce inner variants of these definitions
+* show that strong anodyne extensions are indeed stable under coproducts,
+  transfinite compositions and pushouts (the proof should reduce to the
+  construction of pairings)
+* study the interaction between anodyne extension and binary products:
+  the critical case consists in showing that inclusions
+  `Λ[m, i] ⊗ Δ[n] ∪ Δ[m] ⊗ ∂Δ[n] ⟶ Δ[m] ⊗ Δ[n]` are strong anodyne extensions (@joelriou)
+* show that anodyne extensions are stable under the subdivision functor (@joelriou)
+
+## References
+* [P. Gabriel, M. Zisman, *Calculus of fractions and homotopy theory*, IV.2][gabriel-zisman-1967]
+* [Sean Moss, *Another approach to the Kan-Quillen model structure*][moss-2020]
+
+-/
+
+@[expose] public section
+
+universe u
+
+open CategoryTheory HomotopicalAlgebra Simplicial
+
+namespace SSet
+
+open MorphismProperty
+
+open modelCategoryQuillen in
+/-- In the category of simplicial sets, an anodyne extension is a morphism
+that has the left lifting property with respect to fibrations, where
+a fibration is a morphism that has the right lifting property with respect
+to horn inclusions. We do not introduce a typeclass for anodyne extensions
+because when the Quillen model structure is fully upstreamed (TODO @joelriou),
+the assumption `anodyneExtensions f` can be spelled as
+`[Cofibration f] [WeakEquivalence f]`. -/
+def anodyneExtensions : MorphismProperty SSet.{u} := (fibrations _).llp
+deriving IsMultiplicative, RespectsIso, IsStableUnderCobaseChange,
+  IsStableUnderRetracts, IsStableUnderTransfiniteComposition,
+  IsStableUnderCoproducts
+
+lemma anodyneExtensions.of_isIso {X Y : SSet.{u}} (f : X ⟶ Y) [IsIso f] :
+    anodyneExtensions f :=
+  MorphismProperty.of_isIso anodyneExtensions f
+
+lemma anodyneExtensions_eq_llp_rlp :
+    anodyneExtensions.{u} = modelCategoryQuillen.J.rlp.llp :=
+  rfl
+
+lemma anodyneExtensions.horn_ι {n : ℕ} [NeZero n] (i : Fin (n + 1)) :
+    anodyneExtensions.{u} Λ[n, i].ι := by
+  rw [anodyneExtensions_eq_llp_rlp]
+  exact le_llp_rlp _ _ (modelCategoryQuillen.horn_ι_mem_J n i)
+
+attribute [local instance] Cardinal.fact_isRegular_aleph0
+  Cardinal.orderBotAleph0OrdToType
+
+instance (n : ℕ) : MorphismProperty.IsSmall.{u}
+    (MorphismProperty.ofHoms.{u} (fun (i : Fin (n + 2)) ↦ Λ[n + 1, i].ι)) :=
+  isSmall_ofHoms ..
+
+instance : MorphismProperty.IsSmall.{u} modelCategoryQuillen.J.{u} :=
+  isSmall_iSup ..
+
+instance : IsCardinalForSmallObjectArgument modelCategoryQuillen.J.{u} Cardinal.aleph0.{u} where
+  preservesColimit {A B X Y} i hi f hf := by
+    have : IsFinitelyPresentable.{u} A := by
+      simp only [modelCategoryQuillen.J, iSup_iff] at hi
+      obtain ⟨n, ⟨i⟩⟩ := hi
+      infer_instance
+    infer_instance
+
+instance : HasSmallObjectArgument.{u} modelCategoryQuillen.J.{u} :=
+  ⟨.aleph0, inferInstance, inferInstance, inferInstance⟩
+
+lemma anodyneExtensions_eq_retracts_transfiniteCompositions :
+    anodyneExtensions = (transfiniteCompositions.{u}
+      (coproducts.{u} modelCategoryQuillen.J.{u}).pushouts).retracts := by
+  rw [anodyneExtensions_eq_llp_rlp, llp_rlp_of_hasSmallObjectArgument]
+
+lemma anodyneExtensions_eq_retracts_transfiniteCompositionsOfShape :
+    anodyneExtensions = (transfiniteCompositionsOfShape
+      (coproducts.{u} modelCategoryQuillen.J.{u}).pushouts ℕ).retracts := by
+  rw [anodyneExtensions_eq_llp_rlp,
+    SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0]
+
+/-- In the category of simplicial sets, a strong anodyne extension is a morphism
+which belongs to the closure of horn inclusions by pushouts, coproducts,
+transfinite compositions (but not by retracts). We define this class here
+by saying that `f : X ⟶ Y` is a strong anodyne extension if `f` is a monomorphism
+and there exists a regular pairing (in the sense of Moss) for the subcomplex
+`Subcomplex.range f` of `Y`. -/
+def strongAnodyneExtensions : MorphismProperty SSet.{u} :=
+  fun _ _ f ↦ Mono f ∧ ∃ (P : (Subcomplex.range f).Pairing), P.IsRegular
+
+lemma Subcomplex.Pairing.strongAnodyneExtensions {X : SSet.{u}} {A : X.Subcomplex}
+    (P : A.Pairing) [P.IsRegular] :
+    strongAnodyneExtensions A.ι :=
+  ⟨inferInstance, by
+    generalize h : Subcomplex.range A.ι = B
+    obtain rfl : B = A := by simpa using h.symm
+    exact ⟨P, inferInstance⟩⟩
+
+lemma strongAnodyneExtensions_ι_iff {X : SSet.{u}} (A : X.Subcomplex) :
+    strongAnodyneExtensions A.ι ↔ ∃ (P : A.Pairing), P.IsRegular :=
+  ⟨fun hA ↦ by
+    obtain ⟨_, P, _, rfl⟩ :
+        ∃ (B : X.Subcomplex) (P : B.Pairing), P.IsRegular ∧ B = A := by
+      obtain ⟨_, P, _⟩ := hA
+      exact ⟨_, P, inferInstance, by simp⟩
+    exact ⟨P, inferInstance⟩,
+  fun ⟨P, _⟩ ↦ P.strongAnodyneExtensions⟩
+
+lemma Subcomplex.Pairing.anodyneExtensions {X : SSet.{u}} {A : X.Subcomplex}
+    (P : A.Pairing) [P.IsRegular] :
+    anodyneExtensions A.ι :=
+  transfiniteCompositionsOfShape_le _ _ _
+    ⟨P.rankFunction.relativeCellComplex.toTransfiniteCompositionOfShape, fun j hj ↦ by
+      refine (?_ : (_ : MorphismProperty _) ≤ _ ) _
+        (P.rankFunction.relativeCellComplex.attachCells j hj).pushouts_coproducts
+      simp only [pushouts_le_iff, coproducts_le_iff]
+      rintro _ _ _ ⟨c⟩
+      exact .horn_ι c.index⟩
+
+lemma strongAnodyneExtensions_le_anodyneExtensions :
+    strongAnodyneExtensions.{u} ≤ anodyneExtensions := by
+  rintro X Y f ⟨_, P, _⟩
+  rw [← Subfunctor.toRange_ι f]
+  exact comp_mem _ _ _ (.of_isIso _) P.anodyneExtensions
+
+end SSet

Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean

@@ -46,10 +46,12 @@ which consists of horn inclusions `Λ[n, i].ι : Λ[n, i] ⟶ Δ[n]` (for positi
 def J : MorphismProperty SSet.{u} :=
   ⨆ n, .ofHoms (fun (i : Fin (n + 2)) ↦ Λ[n + 1, i].ι)
 
-lemma horn_ι_mem_J (n : ℕ) (i : Fin (n + 2)) :
-    J (horn.{u} (n + 1) i).ι := by
-  simp only [J, iSup_iff]
-  exact ⟨n, ⟨i⟩⟩
+lemma horn_ι_mem_J (n : ℕ) [NeZero n] (i : Fin (n + 1)) :
+    J (horn.{u} n i).ι := by
+  obtain _ | n := n
+  · exact (NeZero.ne 0 rfl).elim
+  · simp only [J, iSup_iff]
+    exact ⟨n, ⟨i⟩⟩
 
 lemma I_le_monomorphisms : I.{u} ≤ monomorphisms _ := by
   rintro _ _ _ ⟨n⟩

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

@@ -195,8 +195,7 @@ instance InducedCategory.concreteCategory {C : Type u} {D : Type u'} [Category.{
   comp_apply _ _ _ := ConcreteCategory.comp_apply _ _ _
   id_apply _ := ConcreteCategory.id_apply _
 
-open ObjectProperty in
-instance FullSubcategory.concreteCategory {C : Type u} [Category.{v} C]
+instance ObjectProperty.FullSubcategory.concreteCategory {C : Type u} [Category.{v} C]
     {FC : C → C → Type*} {CC : C → Type w} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]
     [ConcreteCategory.{w} C FC]
     (P : ObjectProperty C) : ConcreteCategory P.FullSubcategory (fun X Y => FC X.1 Y.1) where
@@ -207,6 +206,9 @@ instance FullSubcategory.concreteCategory {C : Type u} [Category.{v} C]
   comp_apply _ _ _ := ConcreteCategory.comp_apply _ _ _
   id_apply _ := ConcreteCategory.id_apply _
 
+@[deprecated (since := "2026-04-18")] alias FullSubcategory.concreteCategory :=
+  ObjectProperty.FullSubcategory.concreteCategory
+
 end ConcreteCategory
 
 variable {C : Type u} [Category.{v} C]

Mathlib/CategoryTheory/ConcreteCategory/Forget.lean

@@ -111,10 +111,14 @@ instance InducedCategory.hasForget₂ (f : C → D) : HasForget₂ (InducedCateg
   forget₂ := inducedFunctor f
   forget_comp := rfl
 
-instance FullSubcategory.hasForget₂ (P : ObjectProperty C) : HasForget₂ P.FullSubcategory C where
+instance ObjectProperty.FullSubcategory.hasForget₂ (P : ObjectProperty C) :
+    HasForget₂ P.FullSubcategory C where
   forget₂ := P.ι
   forget_comp := rfl
 
+@[deprecated (since := "2026-04-18")] alias FullSubcategory.hasForget₂ :=
+  ObjectProperty.FullSubcategory.hasForget₂
+
 /-- In order to construct a “partially forgetting” functor, we do not need to verify functor laws;
 it suffices to ensure that compositions agree with `forget₂ C D ⋙ forget D = forget C`.
 -/

Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean

@@ -60,6 +60,18 @@ lemma isSmall_iff_eq_ofHoms :
   · rintro ⟨_, _, _, _, rfl⟩
     infer_instance
 
+instance isSmall_iSup {α : Type*} (W : α → MorphismProperty C)
+    [Small.{w} α] [∀ a, IsSmall.{w} (W a)] :
+    IsSmall.{w} (iSup W) where
+  small_toSet := by
+    rw [toSet_iSup]
+    refine small_of_surjective (f := fun (⟨i, f⟩ : Σ i, (W i).toSet) ↦
+      ⟨f, by rw [Set.mem_iUnion]; exact ⟨i, f.prop⟩⟩) ?_
+    rintro ⟨f, hf⟩
+    simp only [Set.mem_iUnion] at hf
+    obtain ⟨i, hf⟩ := hf
+    exact ⟨⟨i, ⟨_, hf⟩⟩, rfl⟩
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean

@@ -90,6 +90,8 @@ instance llp_isStableUnderCoproductsOfShape (J : Type*) :
   have := fun j ↦ hf j _ hp
   infer_instance
 
+instance : IsStableUnderCoproducts.{w} T.llp where
+
 instance rlp_isStableUnderProductsOfShape (J : Type*) :
     T.rlp.IsStableUnderProductsOfShape J := by
   apply IsStableUnderProductsOfShape.mk

Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean

@@ -477,6 +477,18 @@ lemma llp_rlp_of_isCardinalForSmallObjectArgument' :
     { i := Arrow.homMk (𝟙 _) sq.lift
       r := Arrow.homMk (𝟙 _) (πObj I κ f) }
 
+omit κ in
+attribute [local instance] Cardinal.fact_isRegular_aleph0
+  Cardinal.orderBotAleph0OrdToType in
+lemma llp_rlp_of_isCardinalForSmallObjectArgument_aleph0
+    [I.IsCardinalForSmallObjectArgument Cardinal.aleph0.{w}] :
+    I.rlp.llp = (transfiniteCompositionsOfShape (coproducts.{w} I).pushouts ℕ).retracts := by
+  let e : ℕ ≃o Cardinal.aleph0.{w}.ord.ToType :=
+    ULift.orderIso.{w}.symm.trans
+      (OrderIso.ofRelIsoLT (Nonempty.some (by simp [← Ordinal.type_eq])))
+  rw [SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument' _ Cardinal.aleph0,
+    MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso _ e]
+
 /-- If `κ` is a suitable cardinal for the small object argument for `I : MorphismProperty C`,
 then the class `I.rlp.llp` is exactly the class of morphisms that are retracts
 of transfinite compositions of pushouts of coproducts of maps in `I`. -/

Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean

@@ -264,6 +264,8 @@ instance isStableUnderTransfiniteCompositionOfShape_llp :
   exact (MorphismProperty.arrow_mk_iso_iff _
     (Arrow.isoMk h.isoBot.symm (Iso.refl _))).2 this
 
+instance : MorphismProperty.IsStableUnderTransfiniteComposition.{w} W.llp where
+
 lemma transfiniteCompositionsOfShape_le_llp_rlp :
     W.transfiniteCompositionsOfShape J ≤ W.rlp.llp := by
   have := W.rlp.isStableUnderTransfiniteCompositionOfShape_llp J
@@ -288,7 +290,7 @@ lemma transfiniteCompositions_le_llp_rlp :
 
 lemma transfiniteCompositions_pushouts_coproducts_le_llp_rlp :
     (transfiniteCompositions.{w} (coproducts.{w} W).pushouts) ≤ W.rlp.llp := by
-  simpa using transfiniteCompositions_le_llp_rlp (coproducts.{w} W).pushouts
+  simpa using transfiniteCompositions_le_llp_rlp.{w} (coproducts.{w} W).pushouts
 
 lemma retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp :
     (transfiniteCompositions.{w} (coproducts.{w} W).pushouts).retracts ≤ W.rlp.llp := by