Theorems · Theorem · ring theory

NonUnitalStarSubalgebra.iSupLift_of_mem

∀ {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]
  [inst_11 : Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun x1 x2 => x1 ≤ x2) K}
  {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)}
  {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥T) (hx : ↑x ∈ K i),
  (NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Defined in

Mathlib.Algebra.Star.NonUnitalSubalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringNonUnitalSemiringStarRingModuleNonUnitalSemiringStarRingModuleStarRingIsScalarTowerSMulCommClassStarModuleNonempty