diff --git a/Mathlib.lean b/Mathlib.lean index b3989f4a8562ea..9a9ef6040c78cf 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1499,11 +1499,13 @@ 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.Pairing public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat +public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex public import Mathlib.AlgebraicTopology.SimplicialSet.Basic public import Mathlib.AlgebraicTopology.SimplicialSet.Boundary public import Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations @@ -1543,6 +1545,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne public import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits +public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation public import Mathlib.AlgebraicTopology.SimplicialSet.TopAdj public import Mathlib.AlgebraicTopology.SingularHomology.Basic public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Basic.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Basic.lean new file mode 100644 index 00000000000000..489ac47495412b --- /dev/null +++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Basic.lean @@ -0,0 +1,169 @@ +/- +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) +* use the small object argument to show that any anodyne extensions is indeed + a retract of a transfinite composition of pushouts of coproducts of horn + inclusions (@joelriou) +* 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 0joelriou), +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 diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean index 59a2adf9d5002d..ae49b956529d95 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean @@ -87,6 +87,21 @@ lemma δ_eq_iff (i : Fin (d + 2)) : ⟨fun h ↦ (hxy.existsUnique_δ_cast_simplex hd).unique h (hxy.δ_index hd), by rintro rfl; apply δ_index⟩ +include hxy in +lemma le : x ≤ y := by + have := hxy.δ_index rfl + simp only [cast_simplex_rfl] at this + rw [S.le_def, ← y.subcomplex_cast hxy.dim_eq, Subfunctor.ofSection_le_iff, + ← this] + exact ⟨(SimplexCategory.δ _).op, rfl⟩ + +set_option backward.isDefEq.respectTransparency false in +include hxy in +lemma unique (f : ⦋d⦌ ⟶ ⦋d + 1⦌) [Mono f] + (hf : X.map f.op (y.cast (by rw [hxy.dim_eq, hd])).simplex = (x.cast hd).simplex) : + f = SimplexCategory.δ (hxy.index hd) := + (hxy.cast hd).2.unique ⟨inferInstance, hf⟩ ⟨inferInstance, hxy.δ_index hd⟩ + end end IsUniquelyCodimOneFace diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean index db7323c6db44b3..f9c34a351865eb 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean @@ -134,6 +134,14 @@ lemma ne (x : P.I) (y : P.II) : have : x ∈ P.I ∩ P.II := ⟨hx, hy⟩ simp [P.inter] at this +lemma le [P.IsProper] (x : P.II) : + x.1 ≤ (P.p x).1 := + (P.isUniquelyCodimOneFace x).le + +lemma lt [P.IsProper] (x : P.II) : + x.1 < (P.p x).1 := + lt_of_le_of_ne' (P.le x) (P.ne _ _) + end Pairing end SSet.Subcomplex diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean new file mode 100644 index 00000000000000..df05bbfe6fb08e --- /dev/null +++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean @@ -0,0 +1,633 @@ +/- +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.RelativeCellComplex.Basic +public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank +public import Mathlib.AlgebraicTopology.SimplicialSet.Horn +public import Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms +public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation +public import Mathlib.CategoryTheory.Limits.Types.Pushouts +public import Mathlib.CategoryTheory.Limits.Types.Limits +public import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic + +/-! +# The relative cell complex attached to a rank function for a pairing + +Let `A` be a subcomplex of a simplicial set `X`. Let `P : A.Pairing` +be a proper pairing (in the sense of Moss) and `f : P.RankFunction ι` +a rank function. We show that the inclusion `A.ι` is a relative +cell complex with basic cells given by horn inclusions. + +## References +* [Sean Moss, *Another approach to the Kan-Quillen model structure*][moss-2020] + +-/ + +@[expose] public section + +universe v u + +open CategoryTheory HomotopicalAlgebra Simplicial Limits Opposite + +namespace SSet.Subcomplex.Pairing + +variable {X : SSet.{u}} {A : X.Subcomplex} {P : A.Pairing} + +namespace RankFunction + +variable {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) + +/-- Given a rank function `f : P.RankFunction ι` for a +pairing `P` of a subcomplex `A` of `X : SSet`, and `i : ι`, +this is the type of type (II) simplices of rank `i`. -/ +def Cells (i : ι) : Type u := { s : P.II // f.rank s = i } + +namespace Cells + +variable {f} {i : ι} (c : f.Cells i) + +variable {c} in +@[ext] +lemma ext {c' : f.Cells i} (h : c.1 = c'.1) : c = c' := + Subtype.ext h + +/-- The dimension `c.dim` of a cell `c` of a rank function for a +pairing `P` of a subcomplex of a simplicial set. This is defined +as the dimension of the corresponding type (II) simplex. +(In the case `P` is proper, the corresponding type (I) simplex +will be of dimension `c.dim + 1`.) -/ +abbrev dim : ℕ := c.1.1.dim + +variable [P.IsProper] + +/-- If `c` is a cell of a rank function for a proper pairing `P` +of a subcomplex of a simplicial set, this is the index +in `Fin (c.dim + 2)` of the face of the type (I) simplex +given by the corresponding type (II) simplex. -/ +noncomputable def index : Fin (c.dim + 2) := + (P.isUniquelyCodimOneFace c.1).index rfl + +/-- The horn in the standard simplex corresponding to a cell +of a rank function for a proper pairing of a subcomplex of +a simplicial set. -/ +protected noncomputable abbrev horn : + (Δ[c.dim + 1] : SSet.{u}).Subcomplex := + SSet.horn _ c.index + +/-- The morphism `Δ[c.dim + 1] ⟶ X` corresponding to a cell of rank +function for a proper pairing of a subcomplex of `X : SSet`. -/ +abbrev map : + Δ[c.dim + 1] ⟶ X := + yonedaEquiv.symm + ((P.p c.1).1.cast (P.isUniquelyCodimOneFace c.1).dim_eq).simplex + +@[simp] +lemma range_map : Subcomplex.range c.map = (P.p c.1).1.subcomplex := by + rw [range_eq_ofSimplex, Equiv.apply_symm_apply, S.ofSimplex_eq_subcomplex_mk, + ← S.cast_eq_self _ (P.dim_p c.1)] + rfl + +lemma map_app_objEquiv_symm_δ_index : + c.map.app (op ⦋_⦌) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)) = + c.1.1.simplex := + (P.isUniquelyCodimOneFace c.1).δ_index rfl + +lemma subcomplex_not_le_image_horn : + ¬ c.1.1.subcomplex ≤ c.horn.image c.map := by + intro h + simp only [Subfunctor.ofSection_le_iff, image_obj, Set.mem_image] at h + obtain ⟨x, h₁, h₂⟩ := h + obtain ⟨g, rfl⟩ := stdSimplex.objEquiv.symm.surjective x + dsimp at g + rw [← stdSimplex.map_objEquiv_op_apply, Equiv.apply_symm_apply] at h₂ + have := mono_of_nonDegenerate (x:= ⟨_, c.1.1.nonDegenerate⟩) _ _ _ h₂ + obtain rfl := (P.isUniquelyCodimOneFace c.1).unique rfl _ h₂ + rw [← ofSimplex_le_iff, subcomplex_le_horn_iff, ← stdSimplex.face_singleton_compl] at h₁ + tauto + +lemma image_horn_lt_subcomplex : + c.horn.image c.map < (P.p c.1).1.subcomplex := by + rw [lt_iff_le_and_ne] + refine ⟨by simpa using image_le_range c.horn c.map, + fun h ↦ c.subcomplex_not_le_image_horn (by simpa only [h] using P.le c.1)⟩ + +@[simp] +lemma image_face_index_compl : + (stdSimplex.face {c.index}ᶜ).image c.map = c.1.1.subcomplex := by + rw [stdSimplex.face_singleton_compl, image_ofSimplex] + congr 1 + exact (P.isUniquelyCodimOneFace c.1).δ_index rfl + +end Cells + +variable [P.IsProper] in +/-- The horn inclusion corresponding to a cell of a rank function +for a proper pairing of a subcomplex of a simplicial set. -/ +noncomputable abbrev basicCell (i : ι) (c : f.Cells i) := c.horn.ι + +/-- The filtration of a simplicial set given by a rank function +for a proper pairing of a subcomplex. -/ +def filtration (i : ι) : X.Subcomplex := + A ⊔ ⨆ (j : ι) (_ : j < i) (c : f.Cells j), (P.p c.1).1.subcomplex + +lemma subcomplex_le_filtration {j : ι} (c : f.Cells j) {i : ι} (h : j < i) : + (P.p c.1).1.subcomplex ≤ f.filtration i := by + refine le_trans ?_ le_sup_right + refine le_trans ?_ (le_iSup _ j) + refine le_trans ?_ (le_iSup _ h) + exact le_trans (by rfl) (le_iSup _ c) + +@[simp] +lemma le_filtration (i : ι) : A ≤ f.filtration i := le_sup_left + +@[simp] +lemma filtration_bot [OrderBot ι] : f.filtration ⊥ = A := by + simp [filtration] + +lemma filtration_monotone : Monotone f.filtration := by + intro i₁ i₂ h + rw [filtration] + simp only [sup_le_iff, iSup_le_iff, le_filtration, true_and] + intro j hj c + exact f.subcomplex_le_filtration c (lt_of_lt_of_le hj h) + +lemma filtration_succ [SuccOrder ι] (i : ι) (hi : ¬ IsMax i) : + f.filtration (Order.succ i) = + f.filtration i ⊔ ⨆ (c : f.Cells i), (P.p c.1).1.subcomplex := by + apply le_antisymm + · rw [filtration] + simp only [sup_le_iff, iSup_le_iff] + refine ⟨(f.le_filtration _).trans le_sup_left, fun j hj c ↦ ?_⟩ + rw [Order.lt_succ_iff_of_not_isMax hi] at hj + obtain hj | rfl := hj.lt_or_eq + · exact (f.subcomplex_le_filtration _ hj).trans le_sup_left + · exact le_trans (le_trans (by rfl) (le_iSup _ c)) le_sup_right + · simp only [sup_le_iff, iSup_le_iff] + exact ⟨f.filtration_monotone (Order.le_succ i), + fun c ↦ f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hi)⟩ + +lemma filtration_of_isSuccLimit [OrderBot ι] [SuccOrder ι] + (i : ι) (hi : Order.IsSuccLimit i) : + f.filtration i = ⨆ (j : ι) (_ : j < i), f.filtration j := by + apply le_antisymm + · rw [filtration] + simp only [sup_le_iff, iSup_le_iff] + refine ⟨?_, fun j hj c ↦ ?_⟩ + · refine le_trans ?_ (le_iSup _ ⊥) + exact le_trans (by simp) (le_iSup _ hi.bot_lt) + · refine le_trans ?_ (le_iSup _ (Order.succ j)) + refine le_trans ?_ (le_iSup _ + (by rwa [← Order.IsSuccLimit.succ_lt_iff hi] at hj)) + exact f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hj.not_isMax) + · simp only [iSup_le_iff] + intro j hj + exact f.filtration_monotone hj.le + +lemma iSup_filtration_iio [OrderBot ι] [SuccOrder ι] (m : ι) (hm : Order.IsSuccLimit m) : + ⨆ (i : Set.Iio m), f.filtration i = f.filtration m := + le_antisymm (by + simp only [iSup_le_iff, Subtype.forall, Set.mem_Iio] + intro j hj + exact f.filtration_monotone hj.le) (by + rw [filtration] + simp only [sup_le_iff, iSup_le_iff, ← f.filtration_bot] + exact ⟨le_trans (by rfl) (le_iSup _ ⟨⊥, hm.bot_lt⟩), fun j hj c ↦ + (f.subcomplex_le_filtration c (Order.lt_succ_of_not_isMax (not_isMax_of_lt hj))).trans + (le_trans (by rfl) (le_iSup _ ⟨Order.succ j, hm.succ_lt_iff.2 hj⟩))⟩) + +variable {f} in +lemma Cells.subcomplex_not_le_filtration {j : ι} (x : f.Cells j) : + ¬ x.1.1.subcomplex ≤ f.filtration j := by + rw [ofSimplex_le_iff] + simp only [filtration, Subfunctor.max_obj, Subfunctor.iSup_obj, Set.mem_union, + Set.mem_iUnion, not_or, not_exists] + refine ⟨x.1.1.notMem, fun i hi y h ↦ ?_⟩ + rw [← x.2, ← y.2] at hi + have : P.AncestralRel x.1 y.1 := by + refine ⟨fun hxy ↦ ?_, lt_of_le_of_ne ?_ ((P.ne _ _).symm)⟩ + · rw [hxy] at hi + exact (lt_irrefl _ hi).elim + · rw [← ofSimplex_le_iff] at h + rwa [Subcomplex.N.le_iff, SSet.N.le_iff] + exact lt_irrefl _ (hi.trans (f.lt this)) + +variable [P.IsProper] + +set_option backward.isDefEq.respectTransparency false in +lemma iSup_filtration [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι] : + ⨆ (i : ι), f.filtration i = ⊤ := by + refine le_antisymm (by simp) ?_ + rw [N.subcomplex_le_iff] + intro s _ + induction s using SSet.Subcomplex.N.cases A with + | mem s hs => exact hs.trans (le_trans (by simp) (le_iSup _ ⊥)) + | notMem s => + obtain ⟨t, ht⟩ := P.exists_or s + refine le_trans ?_ + (le_trans (f.subcomplex_le_filtration ⟨t, rfl⟩ (Order.lt_succ _)) (le_iSup _ _)) + obtain rfl | rfl := ht + · exact P.le t + · rfl + +/-- The morphism `Δ[c.dim + 1] ⟶ f.filtration (Order.succ j)` given +by `c : f.Cells j`, when `f` is a rank function for a proper pairing +of a subcomplex of a simplicial set. -/ +def Cells.mapToSucc {j : ι} [SuccOrder ι] [NoMaxOrder ι] (c : f.Cells j) : + Δ[c.dim + 1] ⟶ f.filtration (Order.succ j) := + Subcomplex.lift c.map (by + rw [range_map] + exact f.subcomplex_le_filtration c (Order.lt_succ _)) + +@[reassoc (attr := simp)] +lemma Cells.mapToSucc_ι {j : ι} [SuccOrder ι] [NoMaxOrder ι] (c : f.Cells j) : + c.mapToSucc ≫ (f.filtration (Order.succ j)).ι = c.map := + rfl + +section + +/-- Given a rank function for a proper pairing of a subcomplex of a +simplicial set, this is coproduct of the horns corresponding to +all cells of rank `j`. -/ +noncomputable abbrev sigmaHorn (j : ι) : SSet.{u} := + ∐ fun (c : f.Cells j) ↦ c.horn + +/-- Given a cell `c` of rank `j` for a rank function `f` for a proper +pairing of a subcomplex of a simplicial set, this is the inclusion of +`c.horn` into `f.sigmaHorn j`. -/ +noncomputable abbrev Cells.ιSigmaHorn {j : ι} (c : f.Cells j) : + (c.horn : SSet) ⟶ f.sigmaHorn j := + Sigma.ι (fun (c : f.Cells j) ↦ (c.horn : SSet)) c + +/-- Given a rank function for a proper pairing of a subcomplex of a +simplicial set, this is coproduct of the standard simplices corresponding +to all cells of rank `j`. -/ +noncomputable abbrev sigmaStdSimplex (j : ι) : SSet.{u} := + ∐ fun (i : f.Cells j) ↦ Δ[i.dim + 1] + +/-- Given a cell `c` of rank `j` for a rank function `f` for a proper +pairing of a subcomplex of a simplicial set, this is the inclusion of +`Δ[c.dim + 1]` into `f.sigmaStdSimplex j`. -/ +noncomputable abbrev Cells.ιSigmaStdSimplex {j : ι} (c : f.Cells j) : + Δ[c.dim + 1] ⟶ f.sigmaStdSimplex j := + Sigma.ι (fun (c : f.Cells j) ↦ Δ[c.dim + 1]) c + +lemma ιSigmaHorn_jointly_surjective + {d : ℕ} {j : ι} (a : (f.sigmaHorn j) _⦋d⦌) : + ∃ (c : f.Cells j) (x : (c.horn : SSet) _⦋d⦌), c.ιSigmaHorn.app _ x = a := + Cofan.inj_jointly_surjective_of_isColimit + ((isColimitCofanMkObjOfIsColimit ((CategoryTheory.evaluation _ _).obj _) _ _ + (coproductIsCoproduct _))) a + +omit [P.IsProper] in +lemma ιSigmaStdSimplex_jointly_surjective + {d : ℕ} {j : ι} (a : (f.sigmaStdSimplex j) _⦋d⦌) : + ∃ (c : f.Cells j) (x : Δ[c.dim + 1] _⦋d⦌), c.ιSigmaStdSimplex.app _ x = a := + Cofan.inj_jointly_surjective_of_isColimit + ((isColimitCofanMkObjOfIsColimit ((CategoryTheory.evaluation _ _).obj _) _ _ + (coproductIsCoproduct _))) a + +omit [P.IsProper] in +lemma ιSigmaStdSimplex_eq_iff {j : ι} {d : ℕ} + (x : f.Cells j) (s : (Δ[x.dim + 1] : SSet.{u}) _⦋d⦌) + (y : f.Cells j) (t : (Δ[y.dim + 1] : SSet.{u}) _⦋d⦌) : + x.ιSigmaStdSimplex.app (op ⦋d⦌) s = y.ιSigmaStdSimplex.app (op ⦋d⦌) t ↔ + ∃ (h : x = y), t = cast (by rw [h]) s := + Cofan.inj_apply_eq_iff_of_isColimit + (((isColimitCofanMkObjOfIsColimit ((CategoryTheory.evaluation _ _).obj _) _ _ + (coproductIsCoproduct _)))) _ _ + +instance {j : ι} (c : f.Cells j) : + Mono c.ιSigmaStdSimplex := by + rw [NatTrans.mono_iff_mono_app] + rintro ⟨d⟩ + induction d using SimplexCategory.rec with | _ d + rw [mono_iff_injective] + intro x y h + simpa [f.ιSigmaStdSimplex_eq_iff] using h.symm + +/-- The coproduct of the horn inclusions corresponding to all the cells +of rank `j` for a rank function for a proper pairing of a subcomplex +of a simplicila set. -/ +noncomputable def m (j : ι) : f.sigmaHorn j ⟶ f.sigmaStdSimplex j := + Limits.Sigma.map (basicCell _ _) + +instance (j : ι) : Mono (f.m j) := + MorphismProperty.colimitsOfShape_le (W := .monomorphisms _) _ + (MorphismProperty.colimitsOfShape_colimMap _ (fun ⟨c⟩ ↦ by + dsimp only [Discrete.functor_obj_eq_as, Discrete.natTrans_app] + simp only [MorphismProperty.monomorphisms.iff] + infer_instance)) + +@[reassoc (attr := simp)] +lemma Cells.ι_m {j : ι} (c : f.Cells j) : + c.ιSigmaHorn ≫ f.m j = c.horn.ι ≫ c.ιSigmaStdSimplex := by + simp [m] + +@[simp] +lemma Cells.preimage_filtration_map {j : ι} (c : f.Cells j) : + (f.filtration j).preimage c.map = c.horn := by + refine le_antisymm ?_ ?_ + · simpa only [subcomplex_le_horn_iff, ← Subcomplex.image_le_iff, + Cells.image_face_index_compl] using c.subcomplex_not_le_filtration + · rw [← Subcomplex.image_le_iff, N.subcomplex_le_iff] + intro s hs + induction s using SSet.Subcomplex.N.cases A with + | mem s hs' => exact hs'.trans (by simp) + | notMem s => + obtain ⟨t, ht⟩ := P.exists_or s + rw [← c.prop] + refine le_trans ?_ (f.subcomplex_le_filtration ⟨t, rfl⟩ (f.lt ?_)) + · obtain rfl | rfl := ht + · exact P.le t + · simp + · replace hs : t.1.subcomplex ≤ c.horn.image c.map := by + obtain rfl | rfl := ht + · exact hs + · refine le_trans ?_ hs + rw [← S.le_def] + exact (P.isUniquelyCodimOneFace t).le + refine ⟨?_, ?_⟩ + · rintro rfl + exact c.subcomplex_not_le_image_horn hs + · rw [Subcomplex.N.lt_iff, SSet.N.lt_iff] + exact lt_of_le_of_lt hs (c.image_horn_lt_subcomplex) + +/-- Given a cell `c` of rank `j` for a rank function `f` for a proper +pairing of a subcomplex of a simplicial set, this is the induced +morphism `c.horn ⟶ f.filtration j`. -/ +noncomputable def Cells.mapHorn {j : ι} (c : f.Cells j) : + (c.horn : SSet) ⟶ f.filtration j := + Subcomplex.lift (c.horn.ι ≫ c.map) (by + simp [← image_top, image_le_iff, preimage_comp, c.preimage_filtration_map]) + +@[reassoc (attr := simp)] +lemma Cells.mapHorn_ι {j : ι} (c : f.Cells j) : + c.mapHorn ≫ (f.filtration j).ι = c.horn.ι ≫ c.map := rfl + +/-- Given a rank function `f : P.RankFunction ι` for a proper pairing `P` +of a subcomplex of a simplicial set, this is the induced morphism +`f.sigmaHorn j ⟶ f.filtration j` for any `j : ι`. -/ +noncomputable def t (j : ι) : f.sigmaHorn j ⟶ f.filtration j := + Sigma.desc (fun c ↦ c.mapHorn) + +set_option backward.isDefEq.respectTransparency false in +@[reassoc (attr := simp)] +lemma Cells.ι_t {j : ι} (c : f.Cells j) : + c.ιSigmaHorn ≫ f.t j = c.mapHorn:= by + simp [t] + +/-- Given a rank `j` cell `c` for a rank function `f` for a proper +pairing of a subcomplex of a simplicial set, this is +the nondegenerate simplex in `f.sigmaStdSimplex j` +not in the image of `f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j` +which corresponds to `c.ιSigmaStdSimplex`. -/ +@[simps] +noncomputable def Cells.type₁ {j : ι} (c : f.Cells j) : + (Subcomplex.range (f.m j)).N where + simplex := c.ιSigmaStdSimplex.app _ (stdSimplex.objEquiv.symm (𝟙 _)) + nonDegenerate := by + rw [nonDegenerate_iff_of_mono, + stdSimplex.mem_nonDegenerate_iff_mono, + Equiv.apply_symm_apply] + infer_instance + notMem := by + rintro ⟨y, hy⟩ + obtain ⟨x', ⟨y, hy'⟩, rfl⟩ := f.ιSigmaHorn_jointly_surjective y + rw [← FunctorToTypes.comp, ι_m, FunctorToTypes.comp, + ιSigmaStdSimplex_eq_iff] at hy + obtain ⟨rfl, rfl⟩ := hy + exact objEquiv_symm_notMem_horn_of_isIso _ _ hy' + +/-- Given a rank `j` cell `c` for a rank function `f` for a proper +pairing of a subcomplex of a simplicial set, this is +the nondegenerate simplex in `f.sigmaStdSimplex j` +not in the image of `f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j` +which corresponds to the `c.index`-face of `c.type₁`. -/ +@[simps] +noncomputable def Cells.type₂ {j : ι} (c : f.Cells j) : + (Subcomplex.range (f.m j)).N where + simplex := c.ιSigmaStdSimplex.app _ + (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)) + nonDegenerate := by + rw [nonDegenerate_iff_of_mono, + stdSimplex.mem_nonDegenerate_iff_mono, + Equiv.apply_symm_apply] + infer_instance + notMem := by + rintro ⟨y, hy⟩ + obtain ⟨x', ⟨y, hy'⟩, rfl⟩ := f.ιSigmaHorn_jointly_surjective y + rw [← FunctorToTypes.comp, ι_m, FunctorToTypes.comp, + ιSigmaStdSimplex_eq_iff] at hy + obtain ⟨rfl, rfl⟩ := hy + simpa using (objEquiv_symm_δ_mem_horn_iff _ _).1 hy' + +lemma exists_or_of_range_m_N {j : ι} + (s : (Subcomplex.range (f.m j)).N) : + ∃ (c : f.Cells j), s = c.type₁ ∨ s = c.type₂ := by + obtain ⟨d, s, hs, hs', rfl⟩ := s.mk_surjective + obtain ⟨x, s, rfl⟩ := f.ιSigmaStdSimplex_jointly_surjective s + replace hs' : s ∉ (horn _ x.index).obj _ := + fun h ↦ hs' ⟨x.ιSigmaHorn.app _ ⟨_, h⟩, by simp [← FunctorToTypes.comp]⟩ + obtain ⟨g, rfl⟩ := stdSimplex.objEquiv.symm.surjective s + rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono, + Equiv.apply_symm_apply] at hs + obtain hd | rfl := (SimplexCategory.le_of_mono g).lt_or_eq + · rw [Nat.lt_succ_iff] at hd + obtain hd | rfl := hd.lt_or_eq + · exact (hs' (by simp [horn_obj_eq_top x.index d (by lia)])).elim + · obtain ⟨i, rfl⟩ := SimplexCategory.eq_δ_of_mono g + obtain rfl := (objEquiv_symm_δ_notMem_horn_iff _ _).1 hs' + exact ⟨x, Or.inr rfl⟩ + · obtain rfl := SimplexCategory.eq_id_of_mono g + exact ⟨x, Or.inl rfl⟩ + +variable [SuccOrder ι] [NoMaxOrder ι] + +/-- Given a rank function `f : P.RankFunction ι` for a proper pairing `P` +of a subcomplex of a simplicial set, this is the induced morphism +`f.sigmaStdSimplex j ⟶ f.filtration (Order.succ j)` for any `j : ι`. -/ +noncomputable def b (j : ι) : + f.sigmaStdSimplex j ⟶ f.filtration (Order.succ j) := + Sigma.desc (fun c ↦ c.mapToSucc) + +set_option backward.isDefEq.respectTransparency false in +@[reassoc (attr := simp)] +lemma Cells.ι_b {j : ι} (c : f.Cells j) : + c.ιSigmaStdSimplex ≫ f.b j = c.mapToSucc := by simp [b] + +@[reassoc] +lemma w (j : ι) : + f.t j ≫ homOfLE (f.filtration_monotone (Order.le_succ j)) = f.m j ≫ f.b j := by + ext c : 1 + simp [← cancel_mono (Subcomplex.ι _)] + +lemma isPullback (j : ι) : IsPullback (f.t j) (f.m j) + (homOfLE (f.filtration_monotone (Order.le_succ j))) (f.b j) where + w := f.w j + isLimit' := ⟨evaluationJointlyReflectsLimits _ (fun ⟨d⟩ ↦ by + refine (isLimitMapConePullbackConeEquiv _ _).2 + (IsPullback.isLimit ?_) + induction d using SimplexCategory.rec with | _ d + rw [Types.isPullback_iff] + dsimp + refine ⟨congr_app (f.w j) (op ⦋d⦌), + fun a₁ a₂ h ↦ (mono_iff_injective _).1 + ((NatTrans.mono_iff_mono_app (f.m j)).1 inferInstance _) h.2, fun y b h ↦ ?_⟩ + obtain ⟨x, b, rfl⟩ := f.ιSigmaStdSimplex_jointly_surjective b + have hb : b ∈ Λ[_, x.index].obj _ := by + obtain ⟨y, hy⟩ := y + simp only [← x.preimage_filtration_map] + rw [Subtype.ext_iff] at h + dsimp at h + subst h + rwa [← FunctorToTypes.comp, x.ι_b] at hy + refine ⟨x.ιSigmaHorn.app _ ⟨b, hb⟩, ?_, by simp [← FunctorToTypes.comp]⟩ + rw [Subtype.ext_iff] at h ⊢ + dsimp at h + rw [← FunctorToTypes.comp, x.ι_b] at h + rw [← FunctorToTypes.comp, x.ι_t] + exact h.symm)⟩ + +set_option backward.isDefEq.respectTransparency false in +lemma range_homOfLE_app_union_range_b_app (j : ι) (d : SimplexCategoryᵒᵖ) : + Set.range ((homOfLE (f.filtration_monotone (Order.le_succ j))).app d) ⊔ + Set.range ((f.b j).app d) = Set.univ := by + ext ⟨x, hx⟩ + simp only [filtration, Order.lt_succ_iff, Subfunctor.max_obj, Subfunctor.iSup_obj, Set.mem_union, + Set.mem_iUnion, exists_prop, Subfunctor.toFunctor_obj, Set.sup_eq_union, Set.mem_range, + Subtype.ext_iff, Subfunctor.homOfLe_app_coe, Subtype.exists, exists_eq_right, Set.mem_univ, + iff_true] at hx ⊢ + obtain hx | ⟨i, hi, c, hx⟩ := hx + · exact Or.inl (Or.inl hx) + · obtain hi | rfl := hi.lt_or_eq + · exact Or.inl (Or.inr ⟨i, hi, c, hx⟩) + · rw [← c.range_map, ← c.mapToSucc_ι, ← c.ι_b_assoc] at hx + obtain ⟨y, hy⟩ := hx + exact Or.inr ⟨_, hy⟩ + +/-- Given a rank function `f : P.RankFunction ι` for a proper pairing +of a subcomplex of a simplicial set `X`, this is the simplex of `X` +corresponding to an element in `(Subcomplex.range (f.m j)).N`. -/ +noncomputable def mapN {j : ι} (x : (Subcomplex.range (f.m j)).N) : X.S := + S.mk ((f.b j).app _ x.1.1.2).1 + +@[simp] +lemma mapN_type₁ {j : ι} (c : f.Cells j) : + f.mapN c.type₁ = S.mk (P.p c.1).1.simplex := by + dsimp only [Cells.type₁, mapN] + rw [← S.cast_eq_self _ (P.dim_p c.1)] + dsimp + rw [S.ext_iff, ← FunctorToTypes.comp, c.ι_b] + apply yonedaEquiv_symm_app_id + +@[simp] +lemma mapN_type₂ {j : ι} (c : f.Cells j) : + f.mapN c.type₂ = S.mk c.1.1.simplex := by + dsimp [mapN] + rw [S.ext_iff, ← FunctorToTypes.comp, c.ι_b, Cells.mapToSucc, + lift_app_coe, Cells.map_app_objEquiv_symm_δ_index] + +lemma isPushout_aux₁ {j : ι} + (s : (Subcomplex.range (f.m j)).N) : + (f.mapN s).simplex ∈ SSet.nonDegenerate _ _ := by + obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s + · rw [f.mapN_type₁] + exact (P.p c.1).1.nonDegenerate + · rw [f.mapN_type₂] + exact c.1.1.nonDegenerate + +lemma isPushout_aux₂ {j : ι} : + Function.Injective (f.mapN (j := j)) := by + intro s t h + obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s <;> + obtain ⟨c', rfl | rfl⟩ := f.exists_or_of_range_m_N t <;> + simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq, + ← Subtype.ext_iff] at h + · obtain rfl : c = c' := by + ext : 1 + exact P.p.injective h + rfl + · exact (P.ne _ _ h).elim + · exact (P.ne _ _ h.symm).elim + · rw [h] + +lemma isPushout_aux₃ {j : ι} : + Function.Injective fun (x : (Subcomplex.range (f.m j)).N) ↦ S.mk ((f.b j).app _ x.1.1.2) := + fun _ _ h ↦ f.isPushout_aux₂ (congr_arg (S.map (Subcomplex.ι _)) h) + +set_option backward.isDefEq.respectTransparency false in +lemma isPushout (j : ι) : + IsPushout (f.t j) (f.m j) + (homOfLE (f.filtration_monotone (Order.le_succ j))) (f.b j) where + w := f.w j + isColimit' := ⟨evaluationJointlyReflectsColimits _ (fun ⟨d⟩ ↦ by + induction d using SimplexCategory.rec with | _ d + refine (isColimitMapCoconePushoutCoconeEquiv _ _).2 + (IsPushout.isColimit ?_) + dsimp + refine Types.isPushout_of_isPullback_of_mono' + ((f.isPullback j).map ((CategoryTheory.evaluation _ _).obj _)) + (f.range_homOfLE_app_union_range_b_app _ _) (fun x₁ x₂ hx₁ hx₂ h ↦ ?_) + obtain ⟨s₁, g₁, _, hg₁⟩ := (Subcomplex.range (f.m j)).existsN x₁ hx₁ + obtain ⟨s₂, g₂, _, hg₂⟩ := (Subcomplex.range (f.m j)).existsN x₂ hx₂ + obtain rfl : s₁ = s₂ := f.isPushout_aux₃ (by + dsimp + rw [S.eq_iff_ofSimplex_eq, + ← Subcomplex.ofSimplex_map g₁, ← FunctorToTypes.naturality, + ← Subcomplex.ofSimplex_map g₂, ← FunctorToTypes.naturality, + hg₁, hg₂, h] + all_goals + · rw [Subcomplex.mem_nonDegenerate_iff] + apply f.isPushout_aux₁) + obtain rfl := X.unique_nonDegenerate_map (x := (((f.b _)).app _ x₁).1) + g₁ ⟨_, f.isPushout_aux₁ s₁⟩ (by simp [mapN, ← hg₁, FunctorToTypes.naturality]) + g₂ ⟨_, f.isPushout_aux₁ s₁⟩ (by simp [mapN, h, ← hg₂, FunctorToTypes.naturality]) + rw [← hg₁, hg₂])⟩ + +end + +variable [SuccOrder ι] [OrderBot ι] [NoMaxOrder ι] [WellFoundedLT ι] + +instance : f.filtration_monotone.functor.IsWellOrderContinuous where + nonempty_isColimit m hm := ⟨Preorder.isColimitOfIsLUB _ _ (by + dsimp + rw [← f.iSup_filtration_iio m hm] + apply isLUB_iSup)⟩ + +/-- Given a rank function `f : P.RankFunction ι` for a +proper pairing `P` of a subcomplex `A` of simplicial set `X`, +the inclusion `A.ι` is a relative cell complex with basic cells +given by horn inclusions. -/ +noncomputable def relativeCellComplex : + RelativeCellComplex f.basicCell A.ι where + F := f.filtration_monotone.functor ⋙ Subcomplex.toSSetFunctor + isoBot := Subcomplex.eqToIso (filtration_bot _) + isColimit := + IsColimit.ofIsoColimit (isColimitOfPreserves Subcomplex.toSSetFunctor + (Preorder.colimitCoconeOfIsLUB f.filtration_monotone.functor (pt := ⊤) + (by rw [← f.iSup_filtration]; apply isLUB_iSup)).isColimit) + (Cocone.ext (Subcomplex.topIso _)) + isWellOrderContinuous := + ⟨fun m hm ↦ ⟨isColimitOfPreserves Subcomplex.toSSetFunctor + (Functor.isColimitOfIsWellOrderContinuous f.filtration_monotone.functor m hm)⟩⟩ + incl.app i := (f.filtration i).ι + attachCells j _ := + { ι := f.Cells j + π := id + cofan₁ := _ + cofan₂ := _ + isColimit₁ := colimit.isColimit _ + isColimit₂ := colimit.isColimit _ + m := f.m j + hm c := c.ι_m + g₁ := f.t j + g₂ := f.b j + isPushout := f.isPushout j } + +end RankFunction + +end SSet.Subcomplex.Pairing diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean index 35bedd2a8f0fe6..5da3ed26d0fc91 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean @@ -48,4 +48,9 @@ lemma boundary_eq_iSup (n : ℕ) : simp [stdSimplex.face_obj, boundary, Function.Surjective] tauto +instance {n : ℕ} : HasDimensionLT (boundary n) n := by + rw [boundary_eq_iSup, hasDimensionLT_iSup_iff] + intro i + exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl]) + end SSet diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean b/Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean index 873b6cfa3be7d8..5b55870981194d 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean +++ b/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⟩ diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean index 17211cc2814e1b..7a6bb5136591ec 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean @@ -39,6 +39,10 @@ def horn (n : ℕ) (i : Fin (n + 1)) : (Δ[n] : SSet.{u}).Subcomplex where /-- The `i`-th horn `Λ[n, i]` of the standard `n`-simplex -/ scoped[Simplicial] notation3 "Λ[" n ", " i "]" => SSet.horn (n : ℕ) i +lemma mem_horn_iff {n : ℕ} (i : Fin (n + 1)) {m : SimplexCategoryᵒᵖ} + (x : (Δ[n] : SSet.{u}).obj m) : + x ∈ (horn n i).obj m ↔ Set.range (stdSimplex.asOrderHom x) ∪ {i} ≠ Set.univ := Iff.rfl + set_option backward.isDefEq.respectTransparency false in lemma horn_eq_iSup (n : ℕ) (i : Fin (n + 1)) : horn.{u} n i = @@ -47,6 +51,11 @@ lemma horn_eq_iSup (n : ℕ) (i : Fin (n + 1)) : simp [stdSimplex.face_obj, horn, Set.eq_univ_iff_forall] rfl +instance {n : ℕ} (i : Fin (n + 1)) : HasDimensionLT (horn.{u} n i) n := by + rw [horn_eq_iSup, hasDimensionLT_iSup_iff] + intro i + exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl]) + lemma face_le_horn {n : ℕ} (i j : Fin (n + 1)) (h : i ≠ j) : stdSimplex.face.{u} {i}ᶜ ≤ horn n j := by rw [horn_eq_iSup] @@ -74,6 +83,87 @@ lemma horn_obj_zero (n : ℕ) (i : Fin (n + 3)) : fin_cases a exact Ne.symm hk.2 +set_option backward.isDefEq.respectTransparency false in +lemma horn_obj_eq_top {n : ℕ} (i : Fin (n + 1)) (m : ℕ) (h : m + 1 < n := by lia) : + (horn.{u} n i).obj (op ⦋m⦌) = ⊤ := by + ext x + obtain ⟨f, rfl⟩ := stdSimplex.objEquiv.symm.surjective x + obtain ⟨j, hij, hj⟩ : ∃ (j : Fin (n + 1)), j ≠ i ∧ j ∉ Set.range f.toOrderHom := by + by_contra! + have : Finset.image f.toOrderHom ⊤ ∪ {i} = ⊤ := by ext k; by_cases k = i <;> aesop + have := (congr_arg Finset.card this).symm.le.trans (Finset.card_union_le _ _) + simp only [SimplexCategory.len_mk, Finset.top_eq_univ, Finset.card_univ, Fintype.card_fin, + Finset.card_singleton, add_le_add_iff_right] at this + have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le + lia + simp only [Set.top_eq_univ, horn_eq_iSup, Subfunctor.iSup_obj, Set.iUnion_coe_set, + Set.mem_compl_iff, Set.mem_singleton_iff, Set.mem_iUnion, stdSimplex.mem_face_iff, + Finset.mem_compl, Finset.mem_singleton, exists_prop, Set.mem_univ, iff_true] + exact ⟨j, hij, fun k hk ↦ hj ⟨k, hk⟩⟩ + +lemma subcomplex_le_horn_iff {n : ℕ} + (A : (Δ[n + 1] : SSet.{u}).Subcomplex) (i : Fin (n + 2)) : + A ≤ horn (n + 1) i ↔ ¬ stdSimplex.face {i}ᶜ ≤ A := by + refine ⟨fun hA h ↦ ?_, fun h ↦ ?_⟩ + · replace h := h.trans hA + rw [stdSimplex.face_singleton_compl, Subcomplex.ofSimplex_le_iff, mem_horn_iff] at h + apply h + change Set.range (Fin.succAboveOrderEmb i) ∪ _ = _ + rw [Fin.range_succAboveOrderEmb] + exact Set.compl_union_self {i} + · rw [Subcomplex.le_iff_contains_nonDegenerate] + intro d x hx + by_cases! hd : d < n + · simp [horn_obj_eq_top i d] + · obtain ⟨⟨S, hS⟩, rfl⟩ := stdSimplex.nonDegenerateEquiv'.symm.surjective x + dsimp at hS + simp only [stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le] at hx ⊢ + obtain hd | rfl := hd.lt_or_eq + · obtain rfl : S = .univ := by + rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin] + exact le_antisymm (card_finset_fin_le S) (by lia) + exact (h (le_trans (by simp) hx)).elim + · replace hS : Sᶜ.card = 1 := by + have := S.card_compl_add_card + rw [Fintype.card_fin] at this + lia + obtain ⟨j, rfl⟩ : ∃ j, S = {j}ᶜ := by + rw [Finset.card_eq_one] at hS + obtain ⟨j, hS⟩ := hS + exact ⟨j, by simp [← hS]⟩ + exact face_le_horn _ _ (by rintro rfl; tauto) + +lemma face_le_horn_iff {n : ℕ} (S : Finset (Fin (n + 2))) (j : Fin (n + 2)) : + stdSimplex.face.{u} S ≤ horn (n + 1) j ↔ S ≠ .univ ∧ S ≠ {j}ᶜ := by + rw [subcomplex_le_horn_iff, stdSimplex.face_le_face_iff, ← not_iff_not] + simp only [Finset.le_eq_subset, Decidable.not_not, ne_eq, not_and_or] + refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩ + rw [← Finset.compl_subset_compl, compl_compl, + Finset.subset_singleton_iff, Finset.compl_eq_empty_iff] at h + obtain h | h := h + · exact Or.inl h + · exact Or.inr (by simp [← h]) + +lemma objEquiv_symm_notMem_horn_of_isIso {n : ℕ} (i : Fin (n + 1)) + {d : SimplexCategory} (f : d ⟶ ⦋n⦌) [IsIso f] : + stdSimplex.objEquiv.symm f ∉ (horn.{u} n i).obj (op d) := by + rw [mem_horn_iff, ne_eq, Decidable.not_not] + ext i + simpa using Or.inr ⟨inv f i, by change (inv f ≫ f) i = i; cat_disch⟩ + +lemma objEquiv_symm_δ_mem_horn_iff {n : ℕ} (i j : Fin (n + 2)) : + (stdSimplex.objEquiv (m := op ⦋n⦌)).symm + (SimplexCategory.δ i) ∈ (horn.{u} (n + 1) j).obj (op ⦋n⦌) ↔ i ≠ j := by + dsimp + rw [← Subcomplex.ofSimplex_le_iff, ← stdSimplex.face_singleton_compl, face_le_horn_iff] + simp + +lemma objEquiv_symm_δ_notMem_horn_iff {n : ℕ} (i j : Fin (n + 2)) : + (stdSimplex.objEquiv (m := op ⦋n⦌)).symm + (SimplexCategory.δ i) ∉ (horn.{u} _ j).obj (op ⦋n⦌) ↔ i = j := by + simp [objEquiv_symm_δ_mem_horn_iff.{u}] + + namespace horn open SimplexCategory Finset Opposite diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplices.lean b/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplices.lean index 316fe1700ea0ad..4e839bb7362e5f 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplices.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplices.lean @@ -53,6 +53,14 @@ lemma mk_surjective (x : X.N) : ∃ (n : ℕ) (y : X.nonDegenerate n), x = N.mk _ y.prop := ⟨x.dim, ⟨_, x.nonDegenerate⟩, rfl⟩ +/-- Induction principle for the type `X.N` of nondegenerate simplices of +a simplicial set `X`. -/ +@[elab_as_elim] +def induction {motive : X.N → Sort*} + (mk : ∀ (n : ℕ) (x : X.nonDegenerate n), motive (mk x.1 x.2)) (s : X.N) : + motive s := + mk s.dim ⟨_, s.nonDegenerate⟩ + lemma ext_iff (x y : X.N) : x = y ↔ x.toS = y.toS := by grind [cases SSet.N] @@ -62,6 +70,9 @@ instance : Preorder X.N := Preorder.lift toS lemma le_iff {x y : X.N} : x ≤ y ↔ x.subcomplex ≤ y.subcomplex := Iff.rfl +lemma lt_iff {x y : X.N} : x < y ↔ x.subcomplex < y.subcomplex := + Iff.rfl + lemma le_iff_exists_mono {x y : X.N} : x ≤ y ↔ ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f), X.map f.op y.simplex = x.simplex := by simp only [le_iff, CategoryTheory.Subfunctor.ofSection_le_iff, @@ -136,6 +147,17 @@ lemma iSup_subcomplex_eq_top : rintro ⟨d, s, hs⟩ exact le_trans (by rfl) (le_iSup _ (N.mk _ hs))) +lemma subcomplex_le_iff {A B : X.Subcomplex} : + A ≤ B ↔ ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B := by + rw [Subcomplex.le_iff_contains_nonDegenerate] + refine ⟨fun h s ↦ ?_, fun h n x hx ↦ ?_⟩ + · induction s using N.induction with + | mk n x => + intro hx + simp only [Subfunctor.ofSection_le_iff, mk_dim, mk_simplex] at hx ⊢ + exact h _ _ hx + · simpa using h (N.mk _ x.prop) (by simpa) + end N /-- The map which sends a non degenerate simplex of a simplicial set to @@ -152,6 +174,22 @@ namespace S variable {X} +lemma eq_iff_ofSimplex_eq {X : SSet.{u}} {n m : ℕ} (x : X _⦋n⦌) (y : X _⦋m⦌) + (hx : x ∈ X.nonDegenerate _) (hy : y ∈ X.nonDegenerate _) : + S.mk x = S.mk y ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y := by + trans N.mk x hx = N.mk y hy + · exact (N.ext_iff (N.mk x hx) (N.mk y hy)).symm + · simp only [le_antisymm_iff] + rfl + +lemma subcomplex_eq_of_epi (x y : X.S) (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) [Epi f] + (hf : X.map f.op y.simplex = x.simplex) : + x.subcomplex = y.subcomplex := by + refine le_antisymm ?_ ?_ <;> simp only [Subcomplex.ofSimplex_le_iff] + · exact ⟨_, hf⟩ + · have := isSplitEpi_of_epi f + exact ⟨(section_ f).op, by simp [← hf, ← FunctorToTypes.map_comp_apply, ← op_comp]⟩ + lemma existsUnique_n (x : X.S) : ∃! (y : X.N), y.subcomplex = x.subcomplex := existsUnique_of_exists_of_unique (by obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective @@ -182,6 +220,35 @@ lemma toN_eq_iff {x : X.S} {y : X.N} : x.toN = y ↔ y.subcomplex = x.subcomplex := ⟨by rintro rfl; simp, fun h ↦ x.existsUnique_n.unique (by simp) h⟩ +set_option backward.isDefEq.respectTransparency false in +lemma existsUnique_toNπ {x : X.S} {y : X.N} (hy : x.toN = y) : + ∃! (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌), Epi f ∧ X.map f.op y.simplex = x.simplex := by + obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective + obtain ⟨m, f, _, z, rfl⟩ := X.exists_nonDegenerate x + obtain rfl : y = N.mk _ z.2 := by + rw [toN_eq_iff] at hy + rw [← N.subcomplex_injective_iff, hy] + exact subcomplex_eq_of_epi _ _ f rfl + refine existsUnique_of_exists_of_unique ⟨f, inferInstance, rfl⟩ + (fun f₁ f₂ ⟨_, hf₁⟩ ⟨_, hf₂⟩ ↦ unique_nonDegenerate_map _ _ _ _ hf₁.symm _ _ hf₂.symm) + +/-- Given a simplex `x : X.S` of a simplicial set `X`, this is the unique +(epi)morphism `f : ⦋x.dim⦌ ⟶ ⦋x.toN.dim⦌` such that `x.simplex` is +`X.map f.op x.toN.simplex` where `x.toN : X.N` is the unique nondegenerate +simplex of `X` which generates the same subcomplex as `x`. -/ +noncomputable def toNπ (x : X.S) : ⦋x.dim⦌ ⟶ ⦋x.toN.dim⦌ := + (existsUnique_toNπ rfl).exists.choose + +instance (x : X.S) : Epi x.toNπ := (existsUnique_toNπ rfl).exists.choose_spec.1 + +@[simp] +lemma map_toNπ_op_apply (x : X.S) : + X.map x.toNπ.op x.toN.simplex = x.simplex := (existsUnique_toNπ rfl).exists.choose_spec.2 + +lemma dim_toN_le (x : X.S) : + x.toN.dim ≤ x.dim := + SimplexCategory.le_of_epi x.toNπ + end S end SSet diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean index b386b8cf7d002b..7e26fb99dfb221 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean @@ -57,11 +57,30 @@ lemma ext_iff (x y : A.N) : x = y ↔ x.toN = y.toN := by grind [cases SSet.Subcomplex.N] +variable (A) in +@[elab_as_elim] +lemma cases {motive : X.N → Prop} + (mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s) + (notMem : ∀ (s : A.N), motive s.toN) + (s : X.N) : + motive s := by + by_cases hs : s.subcomplex ≤ A + · exact mem s hs + · exact notMem (.mk' s (by simpa using hs)) + +lemma eq_iff_sMk_eq {X : SSet.{u}} {A : X.Subcomplex} (x y : A.N) : + x = y ↔ S.mk x.1.1.2 = S.mk y.1.1.2 := by + rw [N.ext_iff, SSet.N.ext_iff] + instance : PartialOrder A.N := PartialOrder.lift toN (fun _ _ ↦ by simp [ext_iff]) lemma le_iff {x y : A.N} : x ≤ y ↔ x.toN ≤ y.toN := Iff.rfl + +lemma lt_iff {x y : A.N} : x < y ↔ x.toN < y.toN := + Iff.rfl + section variable (s : A.N) {d : ℕ} (hd : s.dim = d) @@ -81,4 +100,11 @@ end end N +lemma existsN {X : SSet.{u}} {n : ℕ} (s : X _⦋n⦌) {A : X.Subcomplex} + (hs : s ∉ A.obj _) : + ∃ (x : A.N) (f : ⦋n⦌ ⟶ ⦋x.dim⦌), Epi f ∧ X.map f.op x.simplex = s := by + refine ⟨⟨(S.mk s).toN, fun h ↦ hs ?_⟩, ⟨(S.mk s).toNπ, inferInstance, by simp⟩⟩ + simp only [← ofSimplex_le_iff] at h ⊢ + simpa using h + end SSet.Subcomplex diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean index 0613fbdce2c72e..ce08c8c892f20a 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean @@ -102,6 +102,14 @@ lemma ext_iff {n : ℕ} (x y : X _⦋n⦌) : /-- The subcomplex generated by a simplex. -/ abbrev subcomplex (s : X.S) : X.Subcomplex := Subcomplex.ofSimplex s.simplex +lemma ofSimplex_eq_subcomplex_mk {n : ℕ} (x : X _⦋n⦌) : + Subcomplex.ofSimplex x = (S.mk x).subcomplex := rfl + +@[simp] +lemma subcomplex_cast (s : X.S) {d : ℕ} (hd : s.dim = d) : + (s.cast hd).subcomplex = s.subcomplex := by + rw [cast_eq_self] + /-- If `s : X.S` and `t : X.S` are simplices of a simplicial set, `s ≤ t` means that the subcomplex generated by `s` is contained in the subcomplex generated by `t`, see `SSet.S.le_def` and `SSet.S.le_iff`. Note that the diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean index 99a3791f741ea2..dbf6a1ced7fe03 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean @@ -162,6 +162,12 @@ lemma yonedaEquiv_map {n m : SimplexCategory} (f : n ⟶ m) : yonedaEquiv.{u} (stdSimplex.map f) = objEquiv.symm f := yonedaEquiv.symm.injective rfl +lemma map_objEquiv_op_apply + {X : SSet.{u}} {n : SimplexCategory} (x : X.obj (op n)) + {m : SimplexCategoryᵒᵖ} (y : (stdSimplex.obj n).obj m) : + dsimp% X.map (stdSimplex.objEquiv y).op x = (yonedaEquiv.symm x).app m y := by + rfl + lemma yonedaEquiv_symm_app_objEquiv_symm {X : SSet.{u}} {n : SimplexCategory} (x : X.obj (op n)) {m : SimplexCategoryᵒᵖ} (f : unop m ⟶ n) : dsimp% (yonedaEquiv.symm x).app _ (stdSimplex.objEquiv.symm f) = @@ -237,12 +243,32 @@ lemma face_inter_face {n : ℕ} (S₁ S₂ : Finset (Fin (n + 1))) : face S₁ ⊓ face S₂ = face (S₁ ⊓ S₂) := by aesop +set_option backward.isDefEq.respectTransparency false in +@[simp] +lemma face_bot (n : ℕ) : + face.{u} (∅ : Finset (Fin (n + 1))) = ⊥ := by + ext + simpa using Finset.univ_neq_empty _ + +@[simp] +lemma face_univ (n : ℕ) : + face.{u} (.univ : Finset (Fin (n + 1))) = ⊤ := by + ext + dsimp + simp only [Set.mem_univ, iff_true] + apply Finset.subset_univ + end stdSimplex lemma yonedaEquiv_comp {X Y : SSet.{u}} {n : SimplexCategory} (f : stdSimplex.obj n ⟶ X) (g : X ⟶ Y) : yonedaEquiv (f ≫ g) = g.app _ (yonedaEquiv f) := rfl +@[simp] +lemma yonedaEquiv_symm_app_id {X : SSet.{u}} {n : ℕ} (x : X _⦋n⦌) : + (yonedaEquiv.symm x).app _ (yonedaEquiv (𝟙 _)) = x := + yonedaEquiv.symm.injective (by simp [← yonedaEquiv_symm_comp]) + namespace Subcomplex variable {X : SSet.{u}} @@ -447,6 +473,100 @@ noncomputable def facePairIso {n : ℕ} (i j : Fin (n + 1)) (hij : i < j) : stdSimplex.isoOfRepresentableBy (stdSimplex.faceRepresentableBy.{u} _ _ (Fin.orderIsoPair i j hij)) +set_option backward.isDefEq.respectTransparency false in +variable (n) in +lemma bijective_image_objEquiv_toOrderHom_univ (m : ℕ) : + Function.Bijective (fun (⟨x, hx⟩ : (Δ[n] : SSet.{u}).nonDegenerate m) ↦ + (⟨Finset.image (objEquiv x).toOrderHom .univ, by + dsimp + rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective] at hx + rw [Finset.card_image_of_injective _ (by exact hx), Finset.card_univ, + Fintype.card_fin]⟩ : { S : Finset (Fin (n + 1)) | S.card = m + 1 })) := by + constructor + · rintro ⟨x₁, h₁⟩ ⟨x₂, h₂⟩ h₃ + obtain ⟨f₁, rfl⟩ := objEquiv.symm.surjective x₁ + obtain ⟨f₂, rfl⟩ := objEquiv.symm.surjective x₂ + simp only [mem_nonDegenerate_iff_mono, Equiv.apply_symm_apply, + SimplexCategory.mono_iff_injective, SimplexCategory.len_mk] at h₁ h₂ + simp only [Set.mem_setOf_eq, SimplexCategory.len_mk, Equiv.apply_symm_apply, + Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq] at h₃ ⊢ + apply SimplexCategory.Hom.ext + rw [← OrderHom.range_eq_iff h₁ h₂] + ext x + simpa using congr_fun (congrArg Membership.mem h₃) x + · intro ⟨S, hS⟩ + dsimp at hS + let e := monoEquivOfFin S (k := m + 1) (by simpa using hS) + refine ⟨⟨objMk ((OrderHom.Subtype.val _).comp (e.toOrderEmbedding.toOrderHom)), ?_⟩, ?_⟩ + · rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective] + intro a b h + apply e.injective + ext : 1 + exact h + · simp [e, ← Finset.image_image, Finset.image_univ_of_surjective e.surjective] + +/-- Nondegenerate `d`-dimensional simplices of the standard simplex `Δ[n]` +identify to subsets of `Fin (n + 1)` of cardinality `d + 1`. -/ +noncomputable def nonDegenerateEquiv' {n d : ℕ} : (Δ[n] : SSet.{u}).nonDegenerate d ≃ + { S : Finset (Fin (n + 1)) | S.card = d + 1 } := + Equiv.ofBijective _ (bijective_image_objEquiv_toOrderHom_univ n d) + +set_option backward.isDefEq.respectTransparency false in +lemma nonDegenerateEquiv'_iff {n d : ℕ} (x : (Δ[n] : SSet.{u}).nonDegenerate d) (j : Fin (n + 1)) : + j ∈ (nonDegenerateEquiv' x).1 ↔ ∃ (i : Fin (d + 1)), x.1 i = j := by + simp only [Set.mem_setOf_eq, Set.coe_setOf] + dsimp [nonDegenerateEquiv'] + aesop + +set_option backward.isDefEq.respectTransparency false in +/-- If `x` is a nondegenerate `d`-simplex of `Δ[n]`, this is the order isomorphism +between `Fin (d + 1)` and the corresponding subset of `Fin (n + 1)` of cardinality `d + 1`. -/ +noncomputable def orderIsoOfNonDegenerate {n d : ℕ} (x : (Δ[n] : SSet.{u}).nonDegenerate d) : + Fin (d + 1) ≃o (nonDegenerateEquiv' x).1 where + toEquiv := Equiv.ofBijective (fun i ↦ ⟨x.1 i, Finset.mem_image_of_mem _ (by simp)⟩) (by + constructor + · have := (mem_nonDegenerate_iff_mono x.1).1 x.2 + rw [SimplexCategory.mono_iff_injective] at this + exact fun _ _ h ↦ this (by simpa using h) + · rintro ⟨j, hj⟩ + rw [nonDegenerateEquiv'_iff] at hj + aesop) + map_rel_iff' := by + have := (mem_nonDegenerate_iff_mono x.1).1 x.2 + rw [SimplexCategory.mono_iff_injective] at this + intro a b + dsimp + simp only [Subtype.mk_le_mk] + constructor + · rw [← not_lt, ← not_lt] + intro h h' + apply h + obtain h'' | h'' := (monotone_apply x.1 h'.le).lt_or_eq + · assumption + · simp only [this h'', lt_self_iff_false] at h' + · intro h + exact monotone_apply _ h + +lemma face_nonDegenerateEquiv' {n d : ℕ} (x : (Δ[n] : SSet.{u}).nonDegenerate d) : + face (nonDegenerateEquiv' x).1 = Subcomplex.ofSimplex x.1 := + face_eq_ofSimplex.{u} _ _ (orderIsoOfNonDegenerate x) + +set_option backward.isDefEq.respectTransparency false in +lemma nonDegenerateEquiv'_symm_apply_mem {n d : ℕ} + (S : { S : Finset (Fin (n + 1)) | S.card = d + 1 }) (i : Fin (d + 1)) : + (nonDegenerateEquiv'.{u}.symm S).1 i ∈ S.1 := by + obtain ⟨f, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S + dsimp [nonDegenerateEquiv'] + simp only [Equiv.ofBijective_symm_apply_apply, Finset.mem_image, Finset.mem_univ, true_and] + exact ⟨i, rfl⟩ + +lemma nonDegenerateEquiv'_symm_mem_iff_face_le {n d : ℕ} + (S : { S : Finset (Fin (n + 1)) | S.card = d + 1 }) + (A : (Δ[n] : SSet.{u}).Subcomplex) : + (nonDegenerateEquiv'.symm S).1 ∈ A.obj _ ↔ face S ≤ A := by + obtain ⟨x, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S + rw [face_nonDegenerateEquiv' x, Equiv.symm_apply_apply, Subcomplex.ofSimplex_le_iff] + instance (n : SimplexCategory) (d : SimplexCategoryᵒᵖ) : Finite ((stdSimplex.{u}.obj n).obj d) := by rw [objEquiv.finite_iff] @@ -462,6 +582,18 @@ instance {X : SSet.{u}} {n : ℕ} (x : X _⦋n⦌) : rw [← Subcomplex.range_eq_ofSimplex] infer_instance +lemma hasDimensionLT_face {n : ℕ} (S : Finset (Fin (n + 1))) + (d : ℕ) (hd : S.card ≤ d) : + HasDimensionLT (face.{u} S) d := by + generalize hm : S.card = m + obtain _ | m := m + · obtain rfl : S = ∅ := by rwa [← Finset.card_eq_zero] + rw [face_bot] + infer_instance + · rw [← hasDimensionLT_iff_of_iso + (isoOfRepresentableBy (faceRepresentableBy S m (monoEquivOfFin S (by simpa))))] + exact hasDimensionLT_of_le _ (m + 1) _ + end stdSimplex section Examples diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean index a3473a4b447d4f..efc090c68d7d9d 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean @@ -159,6 +159,17 @@ lemma mem_ofSimplex_obj_iff {n : ℕ} (x : X _⦋n⦌) {m : SimplexCategoryᵒ dsimp [ofSimplex, Subfunctor.ofSection] aesop +@[simp] +lemma ofSimplex_map {X : SSet.{u}} {n m : ℕ} (f : ⦋n⦌ ⟶ ⦋m⦌) [Epi f] + (x : X _⦋m⦌) : + ofSimplex (X.map f.op x) = ofSimplex x := by + refine le_antisymm ?_ ?_ + · simp only [Subfunctor.ofSection_le_iff] + exact ⟨f.op, by simp⟩ + · simp only [Subfunctor.ofSection_le_iff] + have := isSplitEpi_of_epi f + exact ⟨(section_ f).op, by simp [← FunctorToTypes.map_comp_apply, ← op_comp]⟩ + section variable (f : X ⟶ Y) @@ -239,6 +250,13 @@ lemma preimage_iSup {ι : Type*} (A : ι → X.Subcomplex) (p : Y ⟶ X) : lemma preimage_iInf {ι : Type*} (A : ι → X.Subcomplex) (p : Y ⟶ X) : (⨅ i, A i).preimage p = ⨅ i, (A i).preimage p := by aesop +lemma preimage_comp {Z : SSet.{u}} (A : Z.Subcomplex) (f : X ⟶ Y) (g : Y ⟶ Z) : + A.preimage (f ≫ g) = (A.preimage g).preimage f := rfl + +set_option backward.isDefEq.respectTransparency false in +@[simp] +lemma preimage_ι (A : X.Subcomplex) : A.preimage A.ι = ⊤ := by aesop + end section diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/SubcomplexEvaluation.lean b/Mathlib/AlgebraicTopology/SimplicialSet/SubcomplexEvaluation.lean new file mode 100644 index 00000000000000..c63edc2a3ee1c5 --- /dev/null +++ b/Mathlib/AlgebraicTopology/SimplicialSet/SubcomplexEvaluation.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2025 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.Subcomplex +public import Mathlib.CategoryTheory.Limits.Preorder +public import Mathlib.CategoryTheory.Limits.Set + +/-! +# The evaluation functor on subcomplexes + +We define an evaluation functor `SSet.Subcomplex.evaluation : X.Subcomplex ⥤ Set (X.obj j)` +when `X : SSet` and `j : SimplexCategoryᵒᵖ`. We use it to show that the functor +`Subcomplex.toSSetFunctor : X.Subcomplex ⥤ SSet` preserves filtered colimits. + +-/ + +@[expose] public section + +universe u + +open CategoryTheory Limits + +namespace SSet.Subcomplex + +/-- The evaluation functor `X.Subcomplex ⥤ Set (X.obj j)` when `X : SSet` +and `j : SimplexCategoryᵒᵖ`. -/ +@[simps] +def evaluation (X : SSet.{u}) (j : SimplexCategoryᵒᵖ) : + X.Subcomplex ⥤ Set (X.obj j) where + obj A := A.obj j + map f := CategoryTheory.homOfLE (leOfHom f j) + +instance {J : Type*} [Category J] {X : SSet.{u}} [IsFilteredOrEmpty J] : + PreservesColimitsOfShape J (Subcomplex.toSSetFunctor (X := X)) where + preservesColimit {F} := + preservesColimit_of_preserves_colimit_cocone + (Preorder.colimitCoconeOfIsLUB F isLUB_iSup).isColimit + (evaluationJointlyReflectsColimits _ (fun j ↦ IsColimit.ofIsoColimit + (isColimitOfPreserves Set.functorToTypes + ((Preorder.colimitCoconeOfIsLUB (F ⋙ evaluation _ j) isLUB_iSup).isColimit)) + (Cocone.ext (Set.functorToTypes.mapIso + (CategoryTheory.eqToIso (by cat_disch)))))) + +end SSet.Subcomplex diff --git a/Mathlib/CategoryTheory/Limits/Types/Coproducts.lean b/Mathlib/CategoryTheory/Limits/Types/Coproducts.lean index 5bbd31219421fb..1a26dcd921c629 100644 --- a/Mathlib/CategoryTheory/Limits/Types/Coproducts.lean +++ b/Mathlib/CategoryTheory/Limits/Types/Coproducts.lean @@ -133,6 +133,13 @@ lemma eq_of_inj_apply_eq_of_isColimit i₁ = i₂ := congr_arg Sigma.fst ((equivOfIsColimit hc).injective (a₁ := ⟨i₁, y₁⟩) (a₂ := ⟨i₂, y₂⟩) h) +lemma inj_apply_eq_iff_of_isColimit + {i₁ i₂ : C} (y₁ : F i₁) (y₂ : F i₂) : + c.inj i₁ y₁ = c.inj i₂ y₂ ↔ ∃ (h : i₁ = i₂), y₂ = cast (by rw [h]) y₁ := by + refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ by subst h₁ h₂; rfl⟩ + obtain rfl := eq_of_inj_apply_eq_of_isColimit hc _ _ h + exact ⟨rfl, (inj_injective_of_isColimit hc i₁ h).symm⟩ + end end CofanTypes @@ -177,6 +184,10 @@ lemma eq_of_inj_apply_eq_of_isColimit (hc : IsColimit c) i₁ = i₂ := CofanTypes.eq_of_inj_apply_eq_of_isColimit ((isColimit_cofanTypes_iff c).2 ⟨hc⟩) _ _ h +lemma inj_apply_eq_iff_of_isColimit (hc : IsColimit c) {i j : C} (x : F i) (y : F j) : + c.inj i x = c.inj j y ↔ ∃ (hij : i = j), y = cast (by rw [hij]) x := + CofanTypes.inj_apply_eq_iff_of_isColimit ((isColimit_cofanTypes_iff c).2 ⟨hc⟩) _ _ + end Cofan namespace Types diff --git a/Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean b/Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean index 6799b2bee8a431..d0317673a56845 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean @@ -61,6 +61,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 diff --git a/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean b/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean index 936af363ac772c..63c7882673c4f6 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean b/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean index b53c3e024b96f3..e32810a60d41e4 100644 --- a/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean +++ b/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean @@ -478,6 +478,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`. -/ diff --git a/Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean b/Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean index 7c4063c214d76d..ed16741dfaab4a 100644 --- a/Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean +++ b/Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean @@ -294,6 +294,8 @@ lemma retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp : rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp] apply transfiniteCompositions_pushouts_coproducts_le_llp_rlp +instance : MorphismProperty.IsStableUnderTransfiniteComposition.{w} W.llp where + end MorphismProperty end CategoryTheory diff --git a/Mathlib/CategoryTheory/Subfunctor/Basic.lean b/Mathlib/CategoryTheory/Subfunctor/Basic.lean index 6c4a89dbe70309..bb44994bd201dd 100644 --- a/Mathlib/CategoryTheory/Subfunctor/Basic.lean +++ b/Mathlib/CategoryTheory/Subfunctor/Basic.lean @@ -109,12 +109,12 @@ lemma sInf_obj (S : Set (Subfunctor F)) (U : C) : (sInf S).obj U = sInf (Set.image (fun T ↦ T.obj U) S) := rfl @[simp] -lemma iSup_obj {ι : Type*} (S : ι → Subfunctor F) (U : C) : +lemma iSup_obj {ι : Sort*} (S : ι → Subfunctor F) (U : C) : (⨆ i, S i).obj U = ⋃ i, (S i).obj U := by simp [iSup, sSup_obj] @[simp] -lemma iInf_obj {ι : Type*} (S : ι → Subfunctor F) (U : C) : +lemma iInf_obj {ι : Sort*} (S : ι → Subfunctor F) (U : C) : (⨅ i, S i).obj U = ⋂ i, (S i).obj U := by simp [iInf, sInf_obj] @@ -130,7 +130,7 @@ lemma max_min (S₁ S₂ T : Subfunctor F) : (S₁ ⊔ S₂) ⊓ T = (S₁ ⊓ T) ⊔ (S₂ ⊓ T) := by aesop -lemma iSup_min {ι : Type*} (S : ι → Subfunctor F) (T : Subfunctor F) : +lemma iSup_min {ι : Sort*} (S : ι → Subfunctor F) (T : Subfunctor F) : (⨆ i, S i) ⊓ T = ⨆ i, S i ⊓ T := by aesop diff --git a/Mathlib/Data/Finset/BooleanAlgebra.lean b/Mathlib/Data/Finset/BooleanAlgebra.lean index 938b4d68a37d10..4ab53df9e7d5de 100644 --- a/Mathlib/Data/Finset/BooleanAlgebra.lean +++ b/Mathlib/Data/Finset/BooleanAlgebra.lean @@ -59,6 +59,10 @@ theorem univ_nontrivial_iff : (Finset.univ : Finset α).Nontrivial ↔ Nontrivial α := by rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff] +lemma univ_neq_empty (α : Type*) [Fintype α] [Nonempty α] : + (Finset.univ : Finset α) ≠ ∅ := + fun h ↦ (Finset.univ_eq_empty_iff.1 h).elim (Classical.arbitrary _) + theorem univ_nontrivial [h : Nontrivial α] : (Finset.univ : Finset α).Nontrivial := univ_nontrivial_iff.mpr h diff --git a/Mathlib/Order/Fin/Basic.lean b/Mathlib/Order/Fin/Basic.lean index 1e8583c8c1c5d2..d948b85721966c 100644 --- a/Mathlib/Order/Fin/Basic.lean +++ b/Mathlib/Order/Fin/Basic.lean @@ -378,6 +378,11 @@ def natAddOrderEmb (n) : Fin m ↪o Fin (n + m) := .ofStrictMono (natAdd n) (str def succAboveOrderEmb (p : Fin (n + 1)) : Fin n ↪o Fin (n + 1) := OrderEmbedding.ofStrictMono (succAbove p) (strictMono_succAbove p) +@[simp] +lemma range_succAboveOrderEmb {n : ℕ} (i : Fin (n + 1)) : + Set.range (Fin.succAboveOrderEmb i) = {i}ᶜ := by + aesop + /-! ### Uniqueness of order isomorphisms -/ variable {α : Type*} [Preorder α] diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index c87d089e3f61f3..05909742a41fca 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -1354,6 +1354,11 @@ noncomputable def toTypeOrderBot {c : Cardinal} (hc : c ≠ 0) : OrderBot c.ord.ToType := Ordinal.toTypeOrderBot (fun h ↦ hc (ord_injective (by simpa using h))) +/-- This can be made a local instance in order to get `⊥` +in `Cardinal.aleph0.ord.ToType`. -/ +abbrev orderBotAleph0OrdToType : OrderBot Cardinal.aleph0.ord.ToType := by + exact Cardinal.toTypeOrderBot Cardinal.aleph0_ne_zero + end Cardinal namespace Ordinal