Theorems · Theorem · nonassociative algebras

NonUnitalSubalgebra.iSupLift_of_mem

∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] {ι : Sort u_1} [inst_7 : Nonempty ι] {K : ι → NonUnitalSubalgebra 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 (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A}
  {hT : T = iSup K} {i : ι} (x : ↥T) (hx : ↑x ∈ K i), (NonUnitalSubalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Defined in

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringNonUnitalNonAssocSemiringModuleNonUnitalNonAssocSemiringModuleIsScalarTowerSMulCommClassNonempty