Lean4
/-- The universal property of the direct limit: maps from the components to another module
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit. -/
noncomputable def lift (g : ∀ i, G i ↪[L] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) : DirectLimit G f ↪[L] P
where
toFun :=
Quotient.lift (fun x : Σˣ f => (g x.1) x.2) fun x y xy =>
by
simp only
obtain ⟨i, hx, hy⟩ := directed_of (· ≤ ·) x.1 y.1
rw [← Hg x.1 i hx, ← Hg y.1 i hy]
exact congr_arg _ ((equiv_iff ..).1 xy)
inj' x y
xy := by
rw [← Quotient.out_eq x, ← Quotient.out_eq y, Quotient.lift_mk, Quotient.lift_mk] at xy
obtain ⟨i, hx, hy⟩ := directed_of (· ≤ ·) x.out.1 y.out.1
rw [← Hg x.out.1 i hx, ← Hg y.out.1 i hy] at xy
rw [← Quotient.out_eq x, ← Quotient.out_eq y, Quotient.eq_iff_equiv, equiv_iff G f hx hy]
exact (g i).injective xy
map_fun' F
x := by
obtain ⟨i, y, rfl⟩ := exists_quotient_mk'_sigma_mk'_eq G f x
change _ = funMap F (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ y)
rw [funMap_quotient_mk'_sigma_mk', ← Function.comp_assoc, Quotient.lift_comp_mk]
simp only [Quotient.lift_mk, Embedding.map_fun]
rfl
map_rel' R
x := by
obtain ⟨i, y, rfl⟩ := exists_quotient_mk'_sigma_mk'_eq G f x
change RelMap R (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ y) ↔ _
rw [relMap_quotient_mk'_sigma_mk' G f, ← (g i).map_rel R y, ← Function.comp_assoc, Quotient.lift_comp_mk]
rfl
