Theorems · Theorem · nonassociative algebras

NonUnitalSubalgebra.iSupLift_inclusion

∀ {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 : ↥(K i)) (h : K i ≤ T),
  (NonUnitalSubalgebra.iSupLift K dir f hf T hT) ((NonUnitalSubalgebra.inclusion h) x) = (f i) x

Defined in

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringNonUnitalNonAssocSemiringModuleNonUnitalNonAssocSemiringModuleIsScalarTowerSMulCommClassNonempty