Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Mathlib.lean

@@ -1333,6 +1333,8 @@ import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
 import Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
 import Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
 import Mathlib.AlgebraicTopology.SimplexCategory.Augmented
+import Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
+import Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
 import Mathlib.AlgebraicTopology.SimplexCategory.Basic
 import Mathlib.AlgebraicTopology.SimplexCategory.Defs
 import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Mathlib/Algebra/Group/Defs.lean

@@ -817,7 +817,7 @@ independent:
 * Without `DivisionMonoid.div_eq_mul_inv`, you can define `/` arbitrarily.
 * Without `DivisionMonoid.inv_inv`, you can consider `WithTop Unit` with `a⁻¹ = ⊤` for all `a`.
 * Without `DivisionMonoid.mul_inv_rev`, you can consider `WithTop α` with `a⁻¹ = a` for all `a`
-  where `α` non commutative.
+  where `α` noncommutative.
 * Without `DivisionMonoid.inv_eq_of_mul`, you can consider any `CommMonoid` with `a⁻¹ = a` for all
   `a`.
 

Mathlib/Algebra/Order/Hom/Basic.lean

@@ -76,7 +76,7 @@ variable {ι F α β γ δ : Type*}
 
 /-- `NonnegHomClass F α β` states that `F` is a type of nonnegative morphisms. -/
 class NonnegHomClass (F : Type*) (α β : outParam Type*) [Zero β] [LE β] [FunLike F α β] : Prop where
-  /-- the image of any element is non negative. -/
+  /-- the image of any element is nonnegative. -/
   apply_nonneg (f : F) : ∀ a, 0 ≤ f a
 
 /-- `SubadditiveHomClass F α β` states that `F` is a type of subadditive morphisms. -/

Mathlib/Algebra/Order/Sub/Basic.lean

@@ -206,7 +206,7 @@ namespace CanonicallyOrderedAdd
 
 variable [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α]
 
--- See note [reducible non instances]
+-- See note [reducible non-instances]
 /-- `Sub` structure in linearly canonically ordered monoid using choice. -/
 noncomputable abbrev toSub : Sub α where
   sub x y := if h : y ≤ x then (exists_add_of_le h).choose else 0

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -363,7 +363,7 @@ instance [Inhabited α] : Inhabited (AsBoolRing α) :=
   ‹Inhabited α›
 
 -- See note [reducible non-instances]
-/-- Every generalized Boolean algebra has the structure of a non unital commutative ring with the
+/-- Every generalized Boolean algebra has the structure of a nonunital commutative ring with the
 following data:
 
 * `a + b` unfolds to `a ∆ b` (symmetric difference)

Mathlib/Algebra/Ring/CentroidHom.lean

@@ -13,7 +13,7 @@ import Mathlib.Algebra.Ring.Subsemiring.Basic
 /-!
 # Centroid homomorphisms
 
-Let `A` be a (non unital, non associative) algebra. The centroid of `A` is the set of linear maps
+Let `A` be a (nonunital, non-associative) algebra. The centroid of `A` is the set of linear maps
 `T` on `A` such that `T` commutes with left and right multiplication, that is to say, for all `a`
 and `b` in `A`,
 $$
@@ -599,7 +599,7 @@ section NonUnitalRing
 
 variable [NonUnitalRing α]
 
--- See note [reducible non instances]
+-- See note [reducible non-instances]
 /-- A prime associative ring has commutative centroid. -/
 abbrev commRing
     (h : ∀ a b : α, (∀ r : α, a * r * b = 0) → a = 0 ∨ b = 0) : CommRing (CentroidHom α) :=

Mathlib/Algebra/Ring/Defs.lean

@@ -386,7 +386,7 @@ instance (priority := 100) CommRing.toAddCommGroupWithOne [s : CommRing α] :
     AddCommGroupWithOne α :=
   { s with }
 
-/-- A domain is a nontrivial semiring such that multiplication by a non zero element
+/-- A domain is a nontrivial semiring such that multiplication by a nonzero element
 is cancellative on both sides. In other words, a nontrivial semiring `R` satisfying
 `∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
 `∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.

Mathlib/Algebra/Star/CentroidHom.lean

@@ -12,7 +12,7 @@ import Mathlib.Algebra.Star.Basic
 /-!
 # Centroid homomorphisms on Star Rings
 
-When a (non unital, non-associative) semiring is equipped with an involutive automorphism the
+When a (nonunital, non-associative) semiring is equipped with an involutive automorphism the
 center of the centroid becomes a star ring in a natural way and the natural mapping of the centre of
 the semiring into the centre of the centroid becomes a *-homomorphism.
 

Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

@@ -17,7 +17,7 @@ the subcomplex generated by the images of all `X.σ i`.
 
 In this file, we obtain `degeneracy_comp_P_infty` which states that
 if `X : SimplicialObject C` with `C` a preadditive category,
-`θ : ⦋n⦌ ⟶ Δ'` is a non injective map in `SimplexCategory`, then
+`θ : ⦋n⦌ ⟶ Δ'` is a non-injective map in `SimplexCategory`, then
 `X.map θ.op ≫ P_infty.f n = 0`. It follows from the more precise
 statement vanishing statement `σ_comp_P_eq_zero` for the `P q`.
 

Mathlib/AlgebraicTopology/SimplexCategory/Augmented.lean

@@ -3,118 +3,6 @@ Copyright (c) 2025 Robin Carlier. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Carlier
 -/
-import Mathlib.CategoryTheory.WithTerminal.Basic
-import Mathlib.AlgebraicTopology.SimplexCategory.Basic
-import Mathlib.AlgebraicTopology.SimplicialObject.Basic
+import Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
 
-/-!
-# The Augmented simplex category
-
-This file defines the `AugmentedSimplexCategory` as the category obtained by adding an initial
-object to `SimplexCategory` (using `CategoryTheory.WithInitial`).
-
-This definition provides a canonical full and faithful inclusion functor
-`inclusion : SimplexCategory ⥤ AugmentedSimplexCategory`.
-
-We prove that functors out of `AugmentedSimplexCategory` are equivalent to augmented cosimplicial
-objects and that functors out of `AugmentedSimplexCategoryᵒᵖ` are equivalent to augmented simplicial
-objects, and we provide a translation of the main constrcutions on augmented (co)simplicial objects
-(i.e `drop`, `point` and `toArrow`) in terms of these equivalences.
-
-## TODOs
-* Define a monoidal structure on `AugmentedSimplexCategory`.
--/
-
-open CategoryTheory
-
-/-- The `AugmentedSimplexCategory` is the category obtained from `SimplexCategory` by adjoining an
-initial object. -/
-def AugmentedSimplexCategory := WithInitial SimplexCategory
-  deriving SmallCategory
-
-namespace AugmentedSimplexCategory
-
-variable {C : Type*} [Category C]
-
-/-- The canonical inclusion from `SimplexCategory` to `AugmentedSimplexCategory`. -/
-@[simps!]
-def inclusion : SimplexCategory ⥤ AugmentedSimplexCategory := WithInitial.incl
-
-instance : inclusion.Full := inferInstanceAs WithInitial.incl.Full
-instance : inclusion.Faithful := inferInstanceAs WithInitial.incl.Faithful
-
-instance : Limits.HasInitial AugmentedSimplexCategory :=
-  inferInstanceAs <| Limits.HasInitial <| WithInitial _
-
-/-- The equivalence between functors out of `AugmentedSimplexCategory` and augmented
-cosimplicial objects. -/
-@[simps!]
-def equivAugmentedCosimplicialObject :
-    (AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C :=
-  WithInitial.equivComma
-
-/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
-dropping the augmentation corresponds to precomposition with
-`inclusion : SimplexCategory ⥤ AugmentedSimplexCategory`. -/
-@[simps!]
-def equivAugmentedCosimplicialObjectFunctorCompDropIso :
-    equivAugmentedCosimplicialObject.functor ⋙ CosimplicialObject.Augmented.drop ≅
-    (Functor.whiskeringLeft _ _ C).obj inclusion :=
-  .refl _
-
-/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
-taking the point of the augmentation corresponds to evaluation at the initial object. -/
-@[simps!]
-def equivAugmentedCosimplicialObjectFunctorCompPointIso :
-    equivAugmentedCosimplicialObject.functor ⋙ CosimplicialObject.Augmented.point ≅
-    ((evaluation _ _).obj .star : (AugmentedSimplexCategory ⥤ C) ⥤ C) :=
-  .refl _
-
-@[deprecated (since := "2025-08-22")] alias equivAugmentedCosimplicialObjecFunctorCompPointIso :=
-  equivAugmentedCosimplicialObjectFunctorCompPointIso
-
-/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
-the arrow attached to the cosimplicial object is the one obtained by evaluation at the unique arrow
-`star ⟶ of [0]`. -/
-@[simps!]
-def equivAugmentedCosimplicialObjectFunctorCompToArrowIso :
-    equivAugmentedCosimplicialObject.functor ⋙ CosimplicialObject.Augmented.toArrow ≅
-    Functor.mapArrowFunctor _ C ⋙
-      (evaluation _ _ |>.obj <| .mk <| WithInitial.homTo <| .mk 0) :=
-  .refl _
-
-/-- The equivalence between functors out of `AugmentedSimplexCategory` and augmented simplicial
-objects. -/
-@[simps!]
-def equivAugmentedSimplicialObject :
-    (AugmentedSimplexCategoryᵒᵖ ⥤ C) ≌ SimplicialObject.Augmented C :=
-  WithInitial.opEquiv SimplexCategory |>.congrLeft |>.trans WithTerminal.equivComma
-
-/-- Through the equivalence `(AugmentedSimplexCategoryᵒᵖ ⥤ C) ≌ SimplicialObject.Augmented C`,
-dropping the augmentation corresponds to precomposition with
-`inclusionᵒᵖ : SimplexCategoryᵒᵖ ⥤ AugmentedSimplexCategoryᵒᵖ`. -/
-@[simps!]
-def equivAugmentedSimplicialObjectFunctorCompDropIso :
-    equivAugmentedSimplicialObject.functor ⋙ SimplicialObject.Augmented.drop ≅
-    (Functor.whiskeringLeft _ _ C).obj inclusion.op :=
-  .refl _
-
-/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
-taking the point of the augmentation corresponds to evaluation at the initial object. -/
-@[simps!]
-def equivAugmentedSimplicialObjectFunctorCompPointIso :
-    equivAugmentedSimplicialObject.functor ⋙ SimplicialObject.Augmented.point ≅
-    (evaluation _ C).obj (.op .star) :=
-  .refl _
-
-/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
-the arrow attached to the cosimplicial object is the one obtained by evaluation at the unique arrow
-`star ⟶ of [0]`. -/
-@[simps!]
-def equivAugmentedSimplicialObjectFunctorCompToArrowIso :
-    equivAugmentedSimplicialObject.functor ⋙ SimplicialObject.Augmented.toArrow ≅
-    Functor.mapArrowFunctor _ C ⋙
-      (evaluation _ _ |>.obj <| .mk <| .op <| WithInitial.homTo <| .mk 0) :=
-  .refl _
-
-end AugmentedSimplexCategory
+deprecated_module (since := "2025-07-05")