English
The Type universe carries an IsIPC structure provided by the isomorphism colimitPointwiseProductToProductColimit.
Русский
Вселенная Type имеет структуру IsIPC, задаваемую изоморфизмом colimitPointwiseProductToProductColimit.
LaTeX
$$IsIPC Type u via isIso (colimitPointwiseProductToProductColimit)$$
Lean4
theorem isIso_colimitPointwiseProductToProductColimit (F : ∀ i, I i ⥤ Type u) :
IsIso (colimitPointwiseProductToProductColimit F) := by
-- We follow the proof in [Kashiwara2006], Prop. 3.1.11(ii)
refine (isIso_iff_bijective _).2 ⟨fun y y' hy => ?_, fun x => ?_⟩
· obtain ⟨ky, yk₀, hyk₀⟩ := Types.jointly_surjective' y
obtain ⟨ky', yk₀', hyk₀'⟩ := Types.jointly_surjective' y'
let k := IsFiltered.max ky ky'
let yk : (pointwiseProduct F).obj k := (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
let yk' : (pointwiseProduct F).obj k := (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
obtain rfl : y = colimit.ι (pointwiseProduct F) k yk := by simp only [k, yk, Types.Colimit.w_apply, hyk₀]
obtain rfl : y' = colimit.ι (pointwiseProduct F) k yk' := by simp only [k, yk', Types.Colimit.w_apply, hyk₀']
dsimp only [pointwiseProduct_obj] at yk yk'
have hch :
∀ (s : α),
∃ (i' : I s) (hi' : k s ⟶ i'),
(F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk) =
(F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk') :=
by
intro s
have hy₁ := congrFun (ι_colimitPointwiseProductToProductColimit_π F k s) yk
have hy₂ := congrFun (ι_colimitPointwiseProductToProductColimit_π F k s) yk'
dsimp only [pointwiseProduct_obj, types_comp_apply] at hy₁ hy₂
rw [← hy, hy₁, Types.FilteredColimit.colimit_eq_iff] at hy₂
obtain ⟨i₀, f₀, g₀, h₀⟩ := hy₂
refine ⟨IsFiltered.coeq f₀ g₀, f₀ ≫ IsFiltered.coeqHom f₀ g₀, ?_⟩
conv_rhs => rw [IsFiltered.coeq_condition]
simp [h₀]
choose k' f hk' using hch
apply Types.colimit_sound' f f
exact Types.limit_ext' _ _ _ (fun ⟨s⟩ => by simpa using hk' _)
· have hch : ∀ (s : α), ∃ (i : I s) (xi : (F s).obj i), colimit.ι (F s) i xi = Pi.π (fun s => colimit (F s)) s x :=
fun s => Types.jointly_surjective' _
choose k p hk using hch
refine ⟨colimit.ι (pointwiseProduct F) k ((Types.productIso _).inv p), ?_⟩
refine Types.limit_ext' _ _ _ (fun ⟨s⟩ => ?_)
have := congrFun (ι_colimitPointwiseProductToProductColimit_π F k s) ((Types.productIso _).inv p)
exact this.trans (by simpa using hk _)
