Theorems · Definition · nonassociative algebras

NonUnitalSubalgebra.iSupLift

{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} →
                      [Nonempty ι] →
                        (K : ι → NonUnitalSubalgebra 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 (NonUnitalSubalgebra.inclusion h)) →
                                (T : NonUnitalSubalgebra R A) → T = iSup K → ↥T →ₙₐ[R] B

Define an algebra homomorphism on a directed supremum of non-unital subalgebras by defining it on each non-unital subalgebra, and proving that it agrees on the intersection of non-unital subalgebras.

Defined in

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringNonUnitalNonAssocSemiringModuleNonUnitalNonAssocSemiringModuleIsScalarTowerSMulCommClassNonempty