English
The trans of two cylinders is Very Good when P and P' are Very Good and A is cofibrant.
Русский
Переход (trans) двух цилиндров является Very Good, когда P и P' являются Very Good и A кофибривантен.
LaTeX
$$$(P.trans P').IsVeryGood$$$
Lean4
instance [IsCofibrant A] (P P' : Cylinder A) [P.IsGood] [P'.IsGood] : (P.trans P').IsGood where
cofibration_i :=
by
let ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl _ _) (P'.i₁ ≫ pushout.inr _ _)
rw [show (P.trans P').i = coprod.map P.i₀ (𝟙 A) ≫ ψ by simp [Precylinder.i, ψ]]
have fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr _ _ :=
by
ext
· simp [ψ, pushout.condition]
· simp [ψ]
have sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr _ _) := by
simpa [ψ] using IsPushout.of_hasPushout P.i₁ P'.i₀
have : Cofibration ψ := by
rw [cofibration_iff]
exact
(cofibrations C).of_isPushout (IsPushout.of_top sq fac (IsPushout.of_coprod_inl_with_id P.i₁ A).flip)
(by rw [← cofibration_iff]; infer_instance)
infer_instance
