Lean4
/-- Define an algebra homomorphism on a directed supremum of non-unital subalgebras by defining
it on each non-unital subalgebra, and proving that it agrees on the intersection of
non-unital subalgebras. -/
noncomputable def iSupLift [Nonempty ι] (K : ι → NonUnitalSubalgebra R A) (dir : Directed (· ≤ ·) K)
(f : ∀ i, K i →ₙₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h))
(T : NonUnitalSubalgebra R A) (hT : T = iSup K) : ↥T →ₙₐ[R] B :=
by
subst hT
exact
{ toFun :=
Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x)
(fun i j x hxi hxj => by
let ⟨k, hik, hjk⟩ := dir i j
simp only
rw [hf i k hik, hf j k hjk]
rfl)
_ (by rw [coe_iSup_of_directed dir])
map_zero' := by
dsimp
exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
map_mul' := by
dsimp
apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
all_goals simp
map_add' := by
dsimp
apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
all_goals simp
map_smul' := fun r => by
dsimp
apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x) (fun _ _ => rfl)
all_goals simp }
