Loogle!

Result

Found 58 declarations mentioning HomotopicalAlgebra.trivialFibrations.

• HomotopicalAlgebra.trivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] : CategoryTheory.MorphismProperty C
• HomotopicalAlgebra.trivialCofibrations_eq_unop 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] : HomotopicalAlgebra.trivialCofibrations C = (HomotopicalAlgebra.trivialFibrations Cᵒᵖ).unop
• HomotopicalAlgebra.trivialFibrations_eq_unop 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithFibrations C] : HomotopicalAlgebra.trivialFibrations C = (HomotopicalAlgebra.trivialCofibrations Cᵒᵖ).unop
• HomotopicalAlgebra.mem_trivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.Fibration f] [HomotopicalAlgebra.WeakEquivalence f] : HomotopicalAlgebra.trivialFibrations C f
• HomotopicalAlgebra.trivialCofibrations_op 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithFibrations C] : HomotopicalAlgebra.trivialCofibrations Cᵒᵖ = (HomotopicalAlgebra.trivialFibrations C).op
• HomotopicalAlgebra.trivialFibrations_op 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] : HomotopicalAlgebra.trivialFibrations Cᵒᵖ = (HomotopicalAlgebra.trivialCofibrations C).op
• HomotopicalAlgebra.mem_trivialFibrations_iff 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] : HomotopicalAlgebra.trivialFibrations C f ↔ HomotopicalAlgebra.Fibration f ∧ HomotopicalAlgebra.WeakEquivalence f
• HomotopicalAlgebra.trivialFibrations_sub_fibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] : HomotopicalAlgebra.trivialFibrations C ≤ HomotopicalAlgebra.fibrations C
• HomotopicalAlgebra.trivialFibrations_sub_weakEquivalences 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] : HomotopicalAlgebra.trivialFibrations C ≤ HomotopicalAlgebra.weakEquivalences C
• HomotopicalAlgebra.instIsMultiplicativeCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] : (HomotopicalAlgebra.cofibrations C).IsMultiplicative
• HomotopicalAlgebra.instIsStableUnderCobaseChangeCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] : (HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange
• HomotopicalAlgebra.instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.fibrations C).IsStableUnderRetracts] [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts] : (HomotopicalAlgebra.trivialFibrations C).IsStableUnderRetracts
• HomotopicalAlgebra.instIsMultiplicativeTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] : (HomotopicalAlgebra.trivialFibrations C).IsMultiplicative
• HomotopicalAlgebra.instIsStableUnderBaseChangeTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] : (HomotopicalAlgebra.trivialFibrations C).IsStableUnderBaseChange
• HomotopicalAlgebra.isStableUnderCoproductsOfShape_cofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] (J : Type w) : (HomotopicalAlgebra.cofibrations C).IsStableUnderCoproductsOfShape J
• HomotopicalAlgebra.isStableUnderProductsOfShape_trivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] (J : Type w) : (HomotopicalAlgebra.trivialFibrations C).IsStableUnderProductsOfShape J
• HomotopicalAlgebra.cofibrations_rlp 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] : (HomotopicalAlgebra.cofibrations C).rlp = HomotopicalAlgebra.trivialFibrations C
• HomotopicalAlgebra.trivialFibrations_llp 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] : (HomotopicalAlgebra.trivialFibrations C).llp = HomotopicalAlgebra.cofibrations C
• HomotopicalAlgebra.instFibrationOfIsWeakFactorizationSystemCofibrationsTrivialFibrationsOfIsIso 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] [CategoryTheory.IsIso f] : HomotopicalAlgebra.Fibration f
• HomotopicalAlgebra.instCofibrationICofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f) : HomotopicalAlgebra.Cofibration h.i
• HomotopicalAlgebra.instFibrationPCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f) : HomotopicalAlgebra.Fibration h.p
• HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f) : HomotopicalAlgebra.WeakEquivalence h.p
• HomotopicalAlgebra.instWeakEquivalenceFstOfIsStableUnderBaseChangeTrivialFibrationsOfFibration 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [(HomotopicalAlgebra.trivialFibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.Fibration g] [HomotopicalAlgebra.WeakEquivalence g] : HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.pullback.fst f g)
• HomotopicalAlgebra.instWeakEquivalenceSndOfIsStableUnderBaseChangeTrivialFibrationsOfFibration 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [(HomotopicalAlgebra.trivialFibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.Fibration f] [HomotopicalAlgebra.WeakEquivalence f] : HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.pullback.snd f g)
• HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.Limits.HasCoproduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Cofibration (f i)] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] : HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.Sigma.map f)
• HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations_1 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] [h₁ : HomotopicalAlgebra.Cofibration f₁] [h₂ : HomotopicalAlgebra.Cofibration f₂] [CategoryTheory.Limits.HasBinaryCoproduct X₁ X₂] [CategoryTheory.Limits.HasBinaryCoproduct Y₁ Y₂] : HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.coprod.map f₁ f₂)
• HomotopicalAlgebra.instWeakEquivalenceMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Fibration (f i)] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] [∀ (i : J), HomotopicalAlgebra.WeakEquivalence (f i)] : HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.Pi.map f)
• HomotopicalAlgebra.ModelCategory.cm5b 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C] : (HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)
• HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] : (HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)
• HomotopicalAlgebra.ModelCategory.mk' 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasFiniteColimits C] [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : HomotopicalAlgebra.ModelCategory C
• HomotopicalAlgebra.ModelCategory.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (categoryWithFibrations : HomotopicalAlgebra.CategoryWithFibrations C := by infer_instance) (categoryWithCofibrations : HomotopicalAlgebra.CategoryWithCofibrations C := by infer_instance) (categoryWithWeakEquivalences : HomotopicalAlgebra.CategoryWithWeakEquivalences C := by infer_instance) (cm1a : CategoryTheory.Limits.HasFiniteLimits C := by infer_instance) (cm1b : CategoryTheory.Limits.HasFiniteColimits C := by infer_instance) (cm2 : (HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty := by infer_instance) (cm3a : (HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts := by infer_instance) (cm3b : (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts := by infer_instance) (cm3c : (HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts := by infer_instance) (cm4a : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p := by intros; infer_instance) (cm4b : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence p], CategoryTheory.HasLiftingProperty i p := by intros; infer_instance) (cm5a : (HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C) := by infer_instance) (cm5b : (HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C) := by infer_instance) : HomotopicalAlgebra.ModelCategory C
• HomotopicalAlgebra.Cylinder.ofFactorizationData 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) : HomotopicalAlgebra.Cylinder A
• HomotopicalAlgebra.Cylinder.instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) [CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.IsFibrant A] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] : HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.Cylinder.ofFactorizationData h).I
• HomotopicalAlgebra.Cylinder.instIsVeryGoodOfFactorizationData 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (HomotopicalAlgebra.Cylinder.ofFactorizationData h).IsVeryGood
• HomotopicalAlgebra.Cylinder.ofFactorizationData_I 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (HomotopicalAlgebra.Cylinder.ofFactorizationData h).I = h.Z
• HomotopicalAlgebra.Cylinder.ofFactorizationData_π 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (HomotopicalAlgebra.Cylinder.ofFactorizationData h).π = h.p
• HomotopicalAlgebra.Cylinder.ofFactorizationData_i₀ 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (HomotopicalAlgebra.Cylinder.ofFactorizationData h).i₀ = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h.i
• HomotopicalAlgebra.Cylinder.ofFactorizationData_i₁ 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (HomotopicalAlgebra.Cylinder.ofFactorizationData h).i₁ = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h.i
• HomotopicalAlgebra.Cylinder.ofFactorizationData_i 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (HomotopicalAlgebra.Cylinder.ofFactorizationData h).i = h.i
• CochainComplex.Plus.modelCategoryQuillen.instHasFactorizationCofibrationsTrivialFibrations 📋 Mathlib.Algebra.Homology.ModelCategory.Injective
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : (HomotopicalAlgebra.cofibrations (CochainComplex.Plus C)).HasFactorization (HomotopicalAlgebra.trivialFibrations (CochainComplex.Plus C))
• HomotopicalAlgebra.CofibrantBrownFactorization.toMapFactorizationData 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.CofibrantBrownFactorization f) : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f
• HomotopicalAlgebra.CofibrantBrownFactorization.s 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.CofibrantBrownFactorization f) : Y ⟶ self.Z
• HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.CofibrantBrownFactorization f) : HomotopicalAlgebra.Cofibration self.s
• HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceS 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) (h : HomotopicalAlgebra.CofibrantBrownFactorization f) : HomotopicalAlgebra.WeakEquivalence h.s
• HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) (h : HomotopicalAlgebra.CofibrantBrownFactorization f) [HomotopicalAlgebra.WeakEquivalence f] : HomotopicalAlgebra.WeakEquivalence h.i
• HomotopicalAlgebra.CofibrantBrownFactorization.s_p 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.CofibrantBrownFactorization f) : CategoryTheory.CategoryStruct.comp self.s self.p = CategoryTheory.CategoryStruct.id Y
• HomotopicalAlgebra.CofibrantBrownFactorization.mk' 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : HomotopicalAlgebra.CofibrantBrownFactorization f
• HomotopicalAlgebra.CofibrantBrownFactorization.s_p_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.CofibrantBrownFactorization f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp self.s (CategoryTheory.CategoryStruct.comp self.p h) = h
• HomotopicalAlgebra.CofibrantBrownFactorization.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (toMapFactorizationData : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f) (s : Y ⟶ toMapFactorizationData.Z) (s_p : CategoryTheory.CategoryStruct.comp s toMapFactorizationData.p = CategoryTheory.CategoryStruct.id Y := by cat_disch) (cofibration_s : HomotopicalAlgebra.Cofibration s := by infer_instance) : HomotopicalAlgebra.CofibrantBrownFactorization f
• HomotopicalAlgebra.CofibrantBrownFactorization.mk'_Z 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : (HomotopicalAlgebra.CofibrantBrownFactorization.mk' f h).Z = h.Z
• HomotopicalAlgebra.CofibrantBrownFactorization.mk'_p 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : (HomotopicalAlgebra.CofibrantBrownFactorization.mk' f h).p = h.p
• HomotopicalAlgebra.CofibrantBrownFactorization.mk'_s 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : (HomotopicalAlgebra.CofibrantBrownFactorization.mk' f h).s = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h.i
• HomotopicalAlgebra.CofibrantBrownFactorization.mk'_i 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : (HomotopicalAlgebra.CofibrantBrownFactorization.mk' f h).i = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h.i
• HomotopicalAlgebra.ModelCategory.hasLiftingProperty_of_joyalTrick 📋 Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] [(HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)] [CategoryTheory.Limits.HasPushouts C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] (h : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p) {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence p] : CategoryTheory.HasLiftingProperty i p
• HomotopicalAlgebra.instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Opposite
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] [(HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)] : (HomotopicalAlgebra.cofibrations Cᵒᵖ).HasFactorization (HomotopicalAlgebra.trivialFibrations Cᵒᵖ)
• HomotopicalAlgebra.instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Opposite
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] [(HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)] : (HomotopicalAlgebra.trivialCofibrations Cᵒᵖ).HasFactorization (HomotopicalAlgebra.fibrations Cᵒᵖ)
• HomotopicalAlgebra.trivialFibrations_over_eq 📋 Mathlib.AlgebraicTopology.ModelCategory.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithFibrations C] : HomotopicalAlgebra.trivialFibrations (CategoryTheory.Over S) = (HomotopicalAlgebra.trivialFibrations C).over
• HomotopicalAlgebra.instHasFactorizationOverCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)] : (HomotopicalAlgebra.cofibrations (CategoryTheory.Over S)).HasFactorization (HomotopicalAlgebra.trivialFibrations (CategoryTheory.Over S))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c