Pullbacks in the category of types

In Type*, the pullback of f : X ⟶ Z and g : Y ⟶ Z is the subtype { p : X × Y // f p.1 = g p.2 } of the product. We show some additional lemmas for pullbacks in the category of types.

instance CategoryTheory.Limits.Types.instHasPullbacksType : HasPullbacks (Type u)

@[reducible, inline]

abbrev CategoryTheory.Limits.Types.PullbackObj {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : Type u

The usual explicit pullback in the category of types, as a subtype of the product. The full LimitCone data is bundled as pullbackLimitCone f g.

Equations

• CategoryTheory.Limits.Types.PullbackObj f g = { p : X × Y // f p.1 = g p.2 }

@[reducible, inline]

abbrev CategoryTheory.Limits.Types.pullbackCone {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : PullbackCone f g

The explicit pullback cone on PullbackObj f g. This is bundled with the IsLimit data as pullbackLimitCone f g.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.Types.pullbackLimitCone {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : LimitCone (cospan f g)

The explicit pullback in the category of types, bundled up as a LimitCone for given f and g.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.Types.pullbackLimitCone_cone {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : (pullbackLimitCone f g).cone = pullbackCone f g

@[simp]

theorem CategoryTheory.Limits.Types.pullbackLimitCone_isLimit {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : (pullbackLimitCone f g).isLimit = (pullbackCone f g).isLimitAux (fun (s : PullbackCone f g) (x : s.pt) => ⟨(s.fst x, s.snd x), ⋯⟩) ⋯ ⋯ ⋯

noncomputable def CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) : c.pt ≃ Types.PullbackObj f g

A limit pullback cone in the category of types identifies to the explicit pullback.

Equations

• CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc = (hc.conePointUniqueUpToIso (CategoryTheory.Limits.Types.pullbackLimitCone f g).isLimit).toEquiv

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fst {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) (x : c.pt) : (↑((equivPullbackObj hc) x)).1 = c.fst x

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_snd {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) (x : c.pt) : (↑((equivPullbackObj hc) x)).2 = c.snd x

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) (x : Types.PullbackObj f g) : c.fst ((equivPullbackObj hc).symm x) = (↑x).1

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) (x : Types.PullbackObj f g) : c.snd ((equivPullbackObj hc).symm x) = (↑x).2

theorem CategoryTheory.Limits.PullbackCone.IsLimit.type_ext {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) {x y : c.pt} (h₁ : c.fst x = c.fst y) (h₂ : c.snd x = c.snd y) : x = y

def CategoryTheory.Limits.PullbackCone.toPullbackObj {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : PullbackCone f g) (x : c.pt) : Types.PullbackObj f g

Given c : PullbackCone f g in the category of types, this is the canonical map c.pt → Types.PullbackObj f g.

Equations

• c.toPullbackObj x = ⟨(c.fst x, c.snd x), ⋯⟩

@[simp]

theorem CategoryTheory.Limits.PullbackCone.toPullbackObj_coe_snd {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : PullbackCone f g) (x : c.pt) : (↑(c.toPullbackObj x)).2 = c.snd x

@[simp]

theorem CategoryTheory.Limits.PullbackCone.toPullbackObj_coe_fst {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : PullbackCone f g) (x : c.pt) : (↑(c.toPullbackObj x)).1 = c.fst x

noncomputable def CategoryTheory.Limits.PullbackCone.isLimitEquivBijective {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : PullbackCone f g) : IsLimit c ≃ Function.Bijective c.toPullbackObj

A pullback cone c in the category of types is limit iff the map c.toPullbackObj : c.pt → Types.PullbackObj f g is a bijection.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.Types.pullbackIsoPullback {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : pullback f g ≅ PullbackObj f g

The pullback given by the instance HasPullbacks (Type u) is isomorphic to the explicit pullback object given by PullbackObj.

Equations

• CategoryTheory.Limits.Types.pullbackIsoPullback f g = (CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj (CategoryTheory.Limits.pullbackIsPullback f g)).toIso

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : pullback f g) : (↑((pullbackIsoPullback f g).hom p)).1 = pullback.fst f g p

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : pullback f g) : (↑((pullbackIsoPullback f g).hom p)).2 = pullback.snd f g p

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (x : (pullbackCone f g).pt) : pullback.fst f g ((pullbackIsoPullback f g).inv x) = (fun (p : (pullbackCone f g).pt) => (↑p).1) x

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd_apply {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (x : (pullbackCone f g).pt) : pullback.snd f g ((pullbackIsoPullback f g).inv x) = (fun (p : (pullbackCone f g).pt) => (↑p).2) x

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (pullbackIsoPullback f g).inv (pullback.fst f g) = fun (p : PullbackObj f g) => (↑p).1

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (pullbackIsoPullback f g).inv (pullback.snd f g) = fun (p : PullbackObj f g) => (↑p).2

theorem CategoryTheory.Limits.Types.range_fst_of_isPullback {P X Y Z : Type u} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) : Set.range fst = f ⁻¹' Set.range g

theorem CategoryTheory.Limits.Types.range_snd_of_isPullback {P X Y Z : Type u} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) : Set.range snd = g ⁻¹' Set.range f

@[simp]

theorem CategoryTheory.Limits.Types.range_pullbackFst {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : Set.range (pullback.fst f g) = f ⁻¹' Set.range g

@[simp]

theorem CategoryTheory.Limits.Types.range_pullbackSnd {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : Set.range (pullback.snd f g) = g ⁻¹' Set.range f

theorem CategoryTheory.Limits.Types.ext_of_isPullback {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} (h : IsPullback t l r b) {x₁ y₁ : X₁} (h₁ : t x₁ = t y₁) (h₂ : l x₁ = l y₁) : x₁ = y₁

theorem CategoryTheory.Limits.Types.exists_of_isPullback {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} (h : IsPullback t l r b) (x₂ : X₂) (x₃ : X₃) (hx : r x₂ = b x₃) : ∃ (x₁ : X₁), t x₁ = x₂ ∧ l x₁ = x₃

theorem CategoryTheory.Limits.Types.isPullback_iff {X₁ X₂ X₃ X₄ : Type u} (t : X₁ ⟶ X₂) (r : X₂ ⟶ X₄) (l : X₁ ⟶ X₃) (b : X₃ ⟶ X₄) : IsPullback t l r b ↔ CategoryStruct.comp t r = CategoryStruct.comp l b ∧ (∀ (x₁ y₁ : X₁), t x₁ = t y₁ ∧ l x₁ = l y₁ → x₁ = y₁) ∧ ∀ (x₂ : X₂) (x₃ : X₃), r x₂ = b x₃ → ∃ (x₁ : X₁), t x₁ = x₂ ∧ l x₁ = x₃