iSupLift — Mathlib

English
The composition of iSupLift with inclusion equals the base f_i.
Русский
Композиция iSupLift и inclusion равна базовому f_i.
LaTeX
$$$ (iSupLift\\ K dir f hf T hT).comp (inclusion h) = f i $$$
Lean4
/-- Define a non-unital star algebra homomorphism on a directed supremum of non-unital star
subalgebras by defining it on each non-unital star subalgebra, and proving that it agrees on the
intersection of non-unital star subalgebras. -/
noncomputable def iSupLift [Nonempty ι] (K : ι → NonUnitalStarSubalgebra 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 : NonUnitalStarSubalgebra 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 only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply, inclusion_mk, Eq.ndrec, id_eq,
          eq_mpr_eq_cast]
        exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
      map_mul' :=
        by
        dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply, inclusion_mk, Eq.ndrec, id_eq,
          eq_mpr_eq_cast, ZeroMemClass.coe_zero, AddSubmonoid.mk_add_mk, Set.inclusion_mk]
        apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
        all_goals simp
      map_add' :=
        by
        dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply, inclusion_mk, Eq.ndrec, id_eq,
          eq_mpr_eq_cast]
        apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
        all_goals simp
      map_smul' := fun r =>
        by
        dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply, inclusion_mk, Eq.ndrec, id_eq,
          eq_mpr_eq_cast]
        apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x) (fun _ _ => rfl)
        all_goals simp
      map_star' :=
        by
        dsimp only [SetLike.coe_sort_coe, NonUnitalStarAlgHom.comp_apply, inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast,
          ZeroMemClass.coe_zero, AddSubmonoid.mk_add_mk, Set.inclusion_mk, MulMemClass.mk_mul_mk,
          NonUnitalAlgHom.toDistribMulActionHom_eq_coe, DistribMulActionHom.toFun_eq_coe,
          NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_mk]
        apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => star x) (fun _ _ => rfl)
        all_goals simp [map_star] }
Похожие утверждения