Type synonym for linear map convolutive ring and intrinsic star

This files provides the type synonym WithConv which we will use in later files to put the convolutive product on linear maps instance and the intrinsic star instance. This is to ensure that we only have one multiplication, one unit, and one star.

This is given for any type A so that we can have WithConv (A →ₗ[R] B), WithConv (A →L[R] B), WithConv (Matrix m n R), etc.

structure WithConv (A : Sort u_1) : Sort (max 1 u_1)

A type synonym for the convolutive product of linear maps and intrinsic star.

The instances for the convolutive product and intrinsic star are only available with this type.

Use WithConv.linearEquiv to coerce into this type.

• toConv :: (
• ofConv : A

  Converts an element of WithConv A back to A.

• )

def WithConv.delabToConv : Lean.PrettyPrinter.Delaborator.Delab

This prevents toConv x being printed as { ofConv := x } by delabStructureInstance.

theorem WithConv.ofConv_toConv {A : Type u_2} (x : A) : (toConv x).ofConv = x

@[simp]

theorem WithConv.toConv_ofConv {A : Type u_2} (x : WithConv A) : toConv x.ofConv = x

theorem WithConv.ofConv_surjective {A : Type u_2} : Function.Surjective ofConv

theorem WithConv.toConv_surjective {A : Type u_2} : Function.Surjective toConv

theorem WithConv.ofConv_injective {A : Type u_2} : Function.Injective ofConv

theorem WithConv.toConv_injective {A : Type u_2} : Function.Injective toConv

theorem WithConv.ofConv_bijective {A : Type u_2} : Function.Bijective ofConv

theorem WithConv.toConv_bijective {A : Type u_2} : Function.Bijective toConv

@[implicit_reducible]

instance WithConv.instCoeFunForall {A : Type u_2} {B : Type u_3} {C : Type u_4} [CoeFun A fun (x : A) => B → C] : CoeFun (WithConv A) fun (x : WithConv A) => B → C

theorem WithConv.ext {A : Type u_2} {x y : WithConv A} (h : x.ofConv = y.ofConv) : x = y

theorem WithConv.ext_iff {A : Type u_2} {x y : WithConv A} : x = y ↔ x.ofConv = y.ofConv

def WithConv.equiv (A : Type u_2) : WithConv A ≃ A

WithConv.ofConv and WithConv.toConv as an equivalence.

@[simp]

theorem WithConv.equiv_apply {A : Type u_2} (x : WithConv A) : (WithConv.equiv A) x = x.ofConv

@[simp]

theorem WithConv.symm_equiv_apply {A : Type u_2} (x : A) : (WithConv.equiv A).symm x = toConv x

instance WithConv.instNontrivial {A : Type u_2} [Nontrivial A] : Nontrivial (WithConv A)

@[implicit_reducible]

instance WithConv.instUnique {A : Type u_2} [Unique A] : Unique (WithConv A)

@[implicit_reducible]

instance WithConv.instDecidableEq {A : Type u_2} [DecidableEq A] : DecidableEq (WithConv A)

@[implicit_reducible]

instance WithConv.instAddMonoid {A : Type u_2} [AddMonoid A] : AddMonoid (WithConv A)

@[implicit_reducible]

instance WithConv.instAddCommMonoid {A : Type u_2} [AddCommMonoid A] : AddCommMonoid (WithConv A)

@[implicit_reducible]

instance WithConv.instAddGroup {A : Type u_2} [AddGroup A] : AddGroup (WithConv A)

@[implicit_reducible]

instance WithConv.instAddCommGroup {A : Type u_2} [AddCommGroup A] : AddCommGroup (WithConv A)

@[implicit_reducible]

instance WithConv.instMulAction {R : Type u_1} {A : Type u_2} [Monoid R] [MulAction R A] : MulAction R (WithConv A)

@[implicit_reducible]

instance WithConv.instAddAction {R : Type u_1} {A : Type u_2} [AddMonoid R] [AddAction R A] : AddAction R (WithConv A)

@[implicit_reducible]

instance WithConv.instDistribMulAction {R : Type u_1} {A : Type u_2} [Monoid R] [AddCommMonoid A] [DistribMulAction R A] : DistribMulAction R (WithConv A)

@[implicit_reducible]

instance WithConv.instModule {R : Type u_1} {A : Type u_2} [Semiring R] [AddCommMonoid A] [Module R A] : Module R (WithConv A)

def WithConv.congr {A : Type u_2} {B : Type u_3} (f : A ≃ B) : WithConv A ≃ WithConv B

Lift an equivalence between A and B to WithConv A and WithConv B.

@[simp]

theorem WithConv.congr_apply {A : Type u_2} {B : Type u_3} (f : A ≃ B) (x : WithConv A) : (WithConv.congr f) x = toConv (f x.ofConv)

@[simp]

theorem WithConv.symm_congr {A : Type u_2} {B : Type u_3} (f : A ≃ B) : (WithConv.congr f).symm = WithConv.congr f.symm

theorem WithConv.symm_congr_apply {A : Type u_2} {B : Type u_3} (f : A ≃ B) (x : WithConv B) : (WithConv.congr f).symm x = toConv (f.symm x.ofConv)

@[simp]

theorem WithConv.toConv_sub {A : Type u_2} [AddGroup A] (x y : A) : toConv (x - y) = toConv x - toConv y

@[simp]

theorem WithConv.ofConv_sub {A : Type u_2} [AddGroup A] (x y : WithConv A) : (x - y).ofConv = x.ofConv - y.ofConv

@[simp]

theorem WithConv.ofConv_neg {A : Type u_2} [AddGroup A] (x : WithConv A) : (-x).ofConv = -x.ofConv

@[simp]

theorem WithConv.toConv_neg {A : Type u_2} [AddGroup A] (x : A) : toConv (-x) = -toConv x

@[simp]

theorem WithConv.ofConv_smul {R : Type u_1} {A : Type u_2} [Monoid R] [MulAction R A] (c : R) (x : WithConv A) : (c • x).ofConv = c • x.ofConv

@[simp]

theorem WithConv.toConv_smul {R : Type u_1} {A : Type u_2} [Monoid R] [MulAction R A] (c : R) (x : A) : toConv (c • x) = c • toConv x

@[simp]

theorem WithConv.ofConv_zero {A : Type u_2} [AddMonoid A] : ofConv 0 = 0

@[simp]

theorem WithConv.toConv_zero {A : Type u_2} [AddMonoid A] : toConv 0 = 0

@[simp]

theorem WithConv.ofConv_add {A : Type u_2} [AddMonoid A] (x y : WithConv A) : (x + y).ofConv = x.ofConv + y.ofConv

@[simp]

theorem WithConv.toConv_add {A : Type u_2} [AddMonoid A] (x y : A) : toConv (x + y) = toConv x + toConv y

@[simp]

theorem WithConv.ofConv_eq_zero {A : Type u_2} [AddMonoid A] {x : WithConv A} : x.ofConv = 0 ↔ x = 0

@[simp]

theorem WithConv.toConv_eq_zero {A : Type u_2} [AddMonoid A] {x : A} : toConv x = 0 ↔ x = 0

def WithConv.addEquiv (A : Type u_2) [AddMonoid A] : WithConv A ≃+ A

The additive equivalence between WithConv A and A.

@[simp]

theorem WithConv.addEquiv_apply (A : Type u_2) [AddMonoid A] (self : WithConv A) : (WithConv.addEquiv A) self = self.ofConv

@[simp]

theorem WithConv.addEquiv_symm_apply_ofConv (A : Type u_2) [AddMonoid A] (ofConv : A) : ((WithConv.addEquiv A).symm ofConv).ofConv = ofConv

@[simp]

theorem WithConv.toEquiv_addEquiv {A : Type u_2} [AddMonoid A] : ↑(WithConv.addEquiv A) = WithConv.equiv A

def WithConv.linearEquiv (R : Type u_1) (A : Type u_2) [AddCommMonoid A] [Semiring R] [Module R A] : WithConv A ≃ₗ[R] A

The linear equivalence between WithConv A and A.

@[simp]

theorem WithConv.linearEquiv_apply {R : Type u_1} {A : Type u_2} [AddCommMonoid A] [Semiring R] [Module R A] (a : WithConv A) : (WithConv.linearEquiv R A) a = a.ofConv

@[simp]

theorem WithConv.symm_linearEquiv_apply {R : Type u_1} {A : Type u_2} [AddCommMonoid A] [Semiring R] [Module R A] (a : A) : (WithConv.linearEquiv R A).symm a = toConv a

@[simp]

theorem WithConv.toAddEquiv_linearEquiv {R : Type u_1} {A : Type u_2} [AddCommMonoid A] [Semiring R] [Module R A] : (WithConv.linearEquiv R A).toAddEquiv = WithConv.addEquiv A

@[simp]

theorem WithConv.ofConv_sum {A : Type u_2} [AddCommMonoid A] {ι : Type u_5} (s : Finset ι) (f : ι → WithConv A) : (∑ i ∈ s, f i).ofConv = ∑ i ∈ s, (f i).ofConv

@[simp]

theorem WithConv.toConv_sum {A : Type u_2} [AddCommMonoid A] {ι : Type u_5} (s : Finset ι) (f : ι → A) : toConv (∑ i ∈ s, f i) = ∑ i ∈ s, toConv (f i)

@[simp]

theorem WithConv.ofConv_listSum {A : Type u_2} [AddCommMonoid A] (l : List (WithConv A)) : l.sum.ofConv = (List.map ofConv l).sum

@[simp]

theorem WithConv.toConv_listSum {A : Type u_2} [AddCommMonoid A] (l : List A) : toConv l.sum = (List.map toConv l).sum

@[simp]

theorem WithConv.ofConv_multisetSum {A : Type u_2} [AddCommMonoid A] (s : Multiset (WithConv A)) : s.sum.ofConv = (Multiset.map ofConv s).sum

@[simp]

theorem WithConv.toConv_multisetSum {A : Type u_2} [AddCommMonoid A] (s : Multiset A) : toConv s.sum = (Multiset.map toConv s).sum

def WithConv.congrLinearEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [AddCommMonoid A] [Semiring R] [Module R A] [AddCommMonoid B] [Module R B] (f : A ≃ₗ[R] B) : WithConv A ≃ₗ[R] WithConv B

Lift a linear equivalence between A and B to WithConv A and WithConv B.

@[simp]

theorem WithConv.congrLinearEquiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [AddCommMonoid A] [Semiring R] [Module R A] [AddCommMonoid B] [Module R B] (f : A ≃ₗ[R] B) (x : WithConv A) : (congrLinearEquiv f) x = toConv (f x.ofConv)

@[simp]

theorem WithConv.symm_congrLinearEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [AddCommMonoid A] [Semiring R] [Module R A] [AddCommMonoid B] [Module R B] (f : A ≃ₗ[R] B) : (congrLinearEquiv f).symm = congrLinearEquiv f.symm

theorem WithConv.symm_congrLinearEquiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [AddCommMonoid A] [Semiring R] [Module R A] [AddCommMonoid B] [Module R B] (f : A ≃ₗ[R] B) (x : WithConv B) : (congrLinearEquiv f).symm x = toConv (f.symm x.ofConv)

@[simp]

theorem WithConv.toEquiv_congrLinearEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [AddCommMonoid A] [Semiring R] [Module R A] [AddCommMonoid B] [Module R B] (f : A ≃ₗ[R] B) : (congrLinearEquiv f).toEquiv = WithConv.congr f.toEquiv