feat(AlgebraicTopology/SimplicialSet): the pushout-product of a mono and an inner anodyne extension is an inner anodyne extension

[mckoen]

A mirror of #39357 for inner anodyne extensions. In particular, the internal hom from a simplicial set to a quasi-category is a quasi-category.

Co-authored-by: Joël Riou

---

• depends on: feat(AlgebraicTopology/SimplicialSet): strong inner anodyne morphisms #38427
• depends on: feat(AlgebraicTopology/SimplicialSet): the pushout-product of a mono and an anodyne extension is an anodyne extension #39357

[github-actions]

PR summary 62c9d10065

Import changes exceeding 2%

%	File
+12.12%	Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
+12.21%	Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations	950	1066	+116 (+12.21%)
Mathlib.AlgebraicTopology.Quasicategory.InnerFibration	957	1073	+116 (+12.12%)

Import changes for all files

Files	Import difference
259 files Mathlib.Algebra.Category.FGModuleCat.Abelian Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Colimits Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.Ring.FinitePresentation Mathlib.Algebra.Category.Ring.Under.Property Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.Birational.Dominant Mathlib.AlgebraicGeometry.Birational.RationalMap Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FlatRank Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Sites.AffineEtale Mathlib.AlgebraicGeometry.Sites.Affine Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.AlgebraicTopology.ModelCategory.Over Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Homotopy Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular Mathlib.AlgebraicTopology.SimplicialSet.Presentable Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism Mathlib.AlgebraicTopology.SimplicialSet.Skeleton Mathlib.AlgebraicTopology.SimplicialSet.TopAdj Mathlib.AlgebraicTopology.SingularHomology.HomologyZero Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Adhesive.Over Mathlib.CategoryTheory.Category.Cat.CartesianClosed Mathlib.CategoryTheory.Category.Cat.Colimit Mathlib.CategoryTheory.Comma.Final Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Filtered.Final Mathlib.CategoryTheory.Filtered.FinallySmall Mathlib.CategoryTheory.Functor.TypeValuedFlat Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.LiftingProperties.PushoutProduct Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.CategoryTheory.Limits.Indization.Equalizers Mathlib.CategoryTheory.Limits.Indization.FilteredColimits Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Limits.Indization.LocallySmall Mathlib.CategoryTheory.Limits.Indization.ParallelPair Mathlib.CategoryTheory.Limits.Indization.Products Mathlib.CategoryTheory.Limits.MorphismProperty Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits Mathlib.CategoryTheory.Limits.Sifted Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition Mathlib.CategoryTheory.LocallyCartesianClosed.Sections Mathlib.CategoryTheory.Monoidal.Arrow Mathlib.CategoryTheory.Monoidal.Braided.Reflection Mathlib.CategoryTheory.Monoidal.Closed.Basic Mathlib.CategoryTheory.Monoidal.Closed.Braided Mathlib.CategoryTheory.Monoidal.Closed.Cartesian Mathlib.CategoryTheory.Monoidal.Closed.Enrichment Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes Mathlib.CategoryTheory.Monoidal.Closed.Functor Mathlib.CategoryTheory.Monoidal.Closed.Ideal Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying Mathlib.CategoryTheory.Monoidal.Closed.Transport Mathlib.CategoryTheory.Monoidal.Closed.Types Mathlib.CategoryTheory.Monoidal.Closed.Zero Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed Mathlib.CategoryTheory.Monoidal.Limits.Colimits Mathlib.CategoryTheory.Monoidal.PushoutProduct Mathlib.CategoryTheory.Monoidal.Rigid.Basic Mathlib.CategoryTheory.Monoidal.Rigid.Braided Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory Mathlib.CategoryTheory.Monoidal.Rigid.Functor Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.MorphismProperty.CommaSites Mathlib.CategoryTheory.MorphismProperty.FunctorCategory Mathlib.CategoryTheory.MorphismProperty.Ind Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.ObjectProperty.Ind Mathlib.CategoryTheory.Pi.Monoidal Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Preadditive.Projective.Internal Mathlib.CategoryTheory.Presentable.Adjunction Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.ColimitPresentation Mathlib.CategoryTheory.Presentable.Dense Mathlib.CategoryTheory.Presentable.Directed Mathlib.CategoryTheory.Presentable.EssentiallyLarge Mathlib.CategoryTheory.Presentable.Finite Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.CategoryTheory.Presentable.Limits Mathlib.CategoryTheory.Presentable.LocallyPresentable Mathlib.CategoryTheory.Presentable.OrthogonalReflection Mathlib.CategoryTheory.Presentable.Presheaf Mathlib.CategoryTheory.Presentable.Retracts Mathlib.CategoryTheory.Presentable.StrongGenerator Mathlib.CategoryTheory.Presentable.Type Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.CoversTop.Over Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime Mathlib.CategoryTheory.Sites.Descent.DescentData Mathlib.CategoryTheory.Sites.Descent.IsPrestack Mathlib.CategoryTheory.Sites.Descent.IsStack Mathlib.CategoryTheory.Sites.Descent.Precoverage Mathlib.CategoryTheory.Sites.LocalProperties Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Sites.Point.Comap Mathlib.CategoryTheory.Sites.Point.Conservative Mathlib.CategoryTheory.Sites.Point.IsMonoidalW Mathlib.CategoryTheory.Sites.Point.Map Mathlib.CategoryTheory.Sites.Point.Monoidal Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered Mathlib.CategoryTheory.Sites.Point.Over Mathlib.CategoryTheory.Sites.Point.Presheaf Mathlib.CategoryTheory.Sites.Point.Skyscraper Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.SubcanonicalOver Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.SmallObject.TransfiniteIteration Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.EffectiveEpi Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.InternallyProjective Mathlib.Condensed.Light.Monoidal Mathlib.Condensed.Light.Sequence Mathlib.Order.Interval.Set.Final Mathlib.RepresentationTheory.Action Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep.Basic Mathlib.RepresentationTheory.Rep.Iso Mathlib.RepresentationTheory.Rep.Res Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Homotopy.TopCat.ToSSet Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy Mathlib.Topology.Sheaves.Points	1
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic	2
Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory	72
6 files Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.InnerFibration Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.KanComplex	116
Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj (new file)	634
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct (new file)	1251

---

Declarations diff (regex)

+ Subcomplex.Pairing.innerAnodyneExtensions
+ Subcomplex.Pairing.strongInnerAnodyneExtensions
+ flipTensor
+ flipTensor_ι
+ for
+ innerAnodyneExtensions.whiskerLeft
+ innerAnodyneExtensions.whiskerRight
+ innerAnodyneExtensions_pushoutObjObjι
+ innerAnodyneExtensions_pushoutObjObjι'
+ innerFibration_pullbackObjObjπ
+ instance (A : SSet.{u}) : Quasicategory ((ihom A).obj (⊤_ _)) := by
+ instance : (cofibrations SSet.{u}).IsMultiplicative := by
+ instance : (cofibrations SSet.{u}).IsStableUnderRetracts := by
+ instance : (fibrations SSet.{u}).IsMultiplicative := by
+ instance : (fibrations SSet.{u}).IsStableUnderRetracts := by
+ instance [MonoidalClosed C] (X : Cᵒᵖ) : (internalHom.obj X).IsRightAdjoint := by
+ instance {A B : SSet.{u}} (i : A ⟶ B) [Mono i] (X : SSet.{u}) [Quasicategory X] :
+ instance {A X : SSet.{u}} [Quasicategory X] : Quasicategory ((ihom A).obj X) := by
+ instance {E B X : SSet.{u}} (p : E ⟶ B) [InnerFibration p] :
+ instance {X : SSet} [Quasicategory X] : InnerFibration (terminal.from X) := by
+ instance {X Y : SSet.{u}} (f : X ⟶ Y) [IsIso f] : Fibration f := by
+ pushoutObjObj
+ pushoutObjObj_ι
+ quasicategory_iff_innerFibration
+ quasicategory_iff_of_isTerminal
+ quasicategory_of_innerFibration
+ rlp_monomorphisms
+ strongInnerAnodyneExtensions
+ strongInnerAnodyneExtensions.mono
+ strongInnerAnodyneExtensions_le_innerAnodyneExtensions
+ strongInnerAnodyneExtensions_le_strongAnodyneExtensions
+ strongInnerAnodyneExtensions_unionProd_ι
+ strongInnerAnodyneExtensions_ι_iff
+ transfiniteCompositionOfShape'
++ innerAnodyneExtensions_unionProd_ι
++ innerAnodyneExtensions_unionProd_ι'
- Quasicategory.from_innerFibrations
- quasicategory_iff_from_innerFibration
- quasicategory_of_from_innerFibrations
- quasicategory_of_innerFibration_quasicategory

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 62c9d10065
Reference commit cca4f7de20

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(AlgebraicTopology/SimplicialSet): strong inner anodyne morphisms #38427
• feat(AlgebraicTopology/SimplicialSet): the pushout-product of a mono and an anodyne extension is an anodyne extension #39357
  By Dependent Issues (🤖). Happy coding!