CategoryTheory.IsPullback.fst_pullbackMap_of_comp_eq
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace CategoryTheory_IsPullback_fst_pullbackMap_of_comp_eq
universe v w u
open _root_.CategoryTheory _root_.CategoryTheory.LimitsLean source · full declaration
theorem _root_.CategoryTheory.IsPullback.fst_pullbackMap_of_comp_eq {C : Type w} [Category.{v} C]
{X X' S T : C}
(f : X ⟶ S) (f' : X' ⟶ S) (t : T ⟶ S) (π : X' ⟶ X) (hπ : π ≫ f = f')
[HasPullback f t] [HasPullback f' t] :
IsPullback (pullback.fst f' t)
(pullback.map f' t f t π (𝟙 T) (𝟙 S)
(by rw [Category.comp_id, hπ]) (by rw [Category.comp_id, Category.id_comp]))
π (pullback.fst f t) := by
have big : IsPullback (pullback.map f' t f t π (𝟙 T) (𝟙 S) (by rw [Category.comp_id, hπ])
(by rw [Category.comp_id, Category.id_comp]) ≫ pullback.snd f t)
(pullback.fst f' t) t (π ≫ f) := by
rw [pullback.lift_snd, Category.comp_id, hπ]
exact (IsPullback.of_hasPullback f' t).flip
exact (IsPullback.of_right big (pullback.lift_fst _ _ _) (IsPullback.of_hasPullback f
t).flip).flip