Theorems · Definition · linear algebra

LinearPMap.sSup

{R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module S F] → (c : Set (E →ₛₗ.[σ] F)) → DirectedOn (fun x1 x2 => x1 ≤ x2) c → E →ₛₗ.[σ] F

For a family of (semi)linear maps with a directed domains such that the one defined on a larger domain restricts to the one defined on the smaller domain, this defines the (semi)linear map defined on the union of the domains extending all the (semi)linear maps in the family.

Defined in

Mathlib.LinearAlgebra.LinearPMap

Cited by

7 results in Mathlib

Foundations

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

Assumes

RingRingAddCommGroupModuleAddCommGroupModule