Theorems · Definition · ring theory

NonUnitalStarSubalgebra.iSupLift

{R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalSemiring A] →
          [inst_2 : StarRing A] →
            [inst_3 : Module R A] →
              [inst_4 : NonUnitalSemiring B] →
                [inst_5 : StarRing B] →
                  [inst_6 : Module R B] →
                    {ι : Type u_1} →
                      [inst_7 : StarRing R] →
                        [inst_8 : IsScalarTower R A A] →
                          [inst_9 : SMulCommClass R A A] →
                            [inst_10 : StarModule R A] →
                              [Nonempty ι] →
                                (K : ι → NonUnitalStarSubalgebra R A) →
                                  Directed (fun x1 x2 => x1 ≤ x2) K →
                                    (f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B) →
                                      (∀ (i j : ι) (h : K i ≤ K j),
                                          f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)) →
                                        (T : NonUnitalStarSubalgebra R A) → T = iSup K → ↥T →⋆ₙₐ[R] B

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.

Defined in

Mathlib.Algebra.Star.NonUnitalSubalgebra

Cited by

5 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringNonUnitalSemiringStarRingModuleNonUnitalSemiringStarRingModuleStarRingIsScalarTowerSMulCommClassStarModuleNonempty