@@ -40,55 +40,70 @@ theorem coe_iSup_of_directed (dir : Directed (· ≤ ·) K) : ↑(iSup K) = ⋃
4040
4141variable (K)
4242
43- -- TODO: turn `hT` into an assumption `T ≤ iSup K`. That's what `Set.iUnionLift` needs
4443/-- Define an algebra homomorphism on a directed supremum of subalgebras by defining
4544it on each subalgebra, and proving that it agrees on the intersection of subalgebras. -/
4645noncomputable def iSupLift (dir : Directed (· ≤ ·) K) (f : ∀ i, K i →ₐ[R] B)
4746 (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h))
48- (T : Subalgebra R A) (hT : T = iSup K) : ↥T →ₐ[R] B :=
49- { toFun := Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x)
50- (fun i j x hxi hxj => by
51- let ⟨k, hik, hjk⟩ := dir i j
52- dsimp
53- rw [hf i k hik, hf j k hjk]
54- rfl)
55- (T : Set A) (by rw [hT, coe_iSup_of_directed dir])
56- map_one' := by apply Set.iUnionLift_const _ (fun _ => 1 ) <;> simp
57- map_zero' := by apply Set.iUnionLift_const _ (fun _ => 0 ) <;> simp
58- map_mul' := by
59- subst hT;
60- apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·)) <;> simp
61- map_add' := by
62- subst hT;
63- apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·)) <;> simp
64- commutes' := fun r => by apply Set.iUnionLift_const _ (fun _ => algebraMap R _ r) <;> simp }
47+ (T : Subalgebra R A) (hT : T ≤ iSup K) : ↥T →ₐ[R] B :=
48+ by
49+ let compat :
50+ ∀ (i j) (x : A) (hxi : x ∈ (K i : Set A)) (hxj : x ∈ (K j : Set A)),
51+ f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩ := by
52+ intro i j x hxi hxj
53+ rcases dir i j with ⟨k, hik, hjk⟩
54+ simp [hf i k hik, hf j k hjk]
55+ let liftSup : ((iSup K : Subalgebra R A)) →ₐ[R] B :=
56+ { toFun :=
57+ Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x) compat
58+ ((iSup K : Subalgebra R A) : Set A)
59+ (le_of_eq <| coe_iSup_of_directed (K := K) dir)
60+ map_one' := by
61+ dsimp
62+ exact Set.iUnionLift_const _ (fun i : ι => (1 : K i)) (fun _ => rfl) _ (by simp)
63+ map_zero' := by
64+ dsimp
65+ exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
66+ map_mul' := by
67+ dsimp
68+ apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· * ·))
69+ all_goals simp
70+ map_add' := by
71+ dsimp
72+ apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· + ·))
73+ all_goals simp
74+ commutes' := fun r => by
75+ dsimp
76+ exact
77+ Set.iUnionLift_const _ (fun i : ι => algebraMap R (K i) r) (fun _ => rfl) _ (by simp) }
78+ exact liftSup.comp (inclusion hT)
6579
6680
6781@[simp]
6882theorem iSupLift_inclusion {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
6983 {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
70- {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : K i) (h : K i ≤ T) :
84+ {T : Subalgebra R A} {hT : T ≤ iSup K} {i : ι} (x : K i) (h : K i ≤ T) :
7185 iSupLift K dir f hf T hT (inclusion h x) = f i x := by
7286 dsimp [iSupLift, inclusion]
7387 rw [Set.iUnionLift_inclusion]
88+ exact SetLike.coe_subset_coe.mpr fun ⦃x⦄ a ↦ hT (h a)
7489
7590@[simp]
7691theorem iSupLift_comp_inclusion {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
7792 {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
78- {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T) :
93+ {T : Subalgebra R A} {hT : T ≤ iSup K} {i : ι} (h : K i ≤ T) :
7994 (iSupLift K dir f hf T hT).comp (inclusion h) = f i := by ext; simp
8095
8196@[simp]
8297theorem iSupLift_mk {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
8398 {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
84- {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : K i) (hx : (x : A) ∈ T) :
99+ {T : Subalgebra R A} {hT : T ≤ iSup K} {i : ι} (x : K i) (hx : (x : A) ∈ T) :
85100 iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x := by
86101 dsimp [iSupLift, inclusion]
87102 rw [Set.iUnionLift_mk]
88103
89104theorem iSupLift_of_mem {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
90105 {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
91- {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : T) (hx : (x : A) ∈ K i) :
106+ {T : Subalgebra R A} {hT : T ≤ iSup K} {i : ι} (x : T) (hx : (x : A) ∈ K i) :
92107 iSupLift K dir f hf T hT x = f i ⟨x, hx⟩ := by
93108 dsimp [iSupLift, inclusion]
94109 rw [Set.iUnionLift_of_mem]
0 commit comments