Skip to content

chore: remove duplicated MulDistribMulAction instances#866

Merged
kbuzzard merged 1 commit intoImperialCollegeLondon:mainfrom
dwrensha:MulDistribMulAction-dedup
Feb 26, 2026
Merged

chore: remove duplicated MulDistribMulAction instances#866
kbuzzard merged 1 commit intoImperialCollegeLondon:mainfrom
dwrensha:MulDistribMulAction-dedup

Conversation

@dwrensha
Copy link
Contributor

There are currently three identical copies of the same instance:

noncomputable
instance {A : Type*} [CommRing A] [Bialgebra K A] :
MulDistribMulAction (L ≃ₐ[K] L) (A →ₐ[K] L) where
smul_mul r f g := by
ext x
change r (Algebra.TensorProduct.lift _ _ (fun _ _ ↦ .all _ _) (Coalgebra.comul x)) =
Algebra.TensorProduct.lift _ _ (fun _ _ ↦ .all _ _) (Coalgebra.comul x)
induction Coalgebra.comul (R := K) x with
| zero => simp only [map_zero]
| add x y _ _ => simp only [map_add, *]
| tmul x y => simp; rfl
smul_one r := by
ext x
change r (algebraMap _ _ _) = _
simp
rfl
noncomputable
instance {A : Type*} [CommRing A] [Bialgebra K A] :
MulDistribMulAction (L ≃ₐ[K] L) (A →ₐ[K] L) where
smul_mul r f g := by
ext x
change r (Algebra.TensorProduct.lift _ _ (fun _ _ ↦ .all _ _) (Coalgebra.comul x)) =
Algebra.TensorProduct.lift _ _ (fun _ _ ↦ .all _ _) (Coalgebra.comul x)
induction Coalgebra.comul (R := K) x with
| zero => simp only [map_zero]
| add x y _ _ => simp only [map_add, *]
| tmul x y => simp; rfl
smul_one r := by
ext x
change r (algebraMap _ _ _) = _
simp
rfl
noncomputable
instance {A : Type*} [CommRing A] [Bialgebra K A] :
MulDistribMulAction (L ≃ₐ[K] L) (A →ₐ[K] L) where
smul_mul r f g := by
ext x
change r (Algebra.TensorProduct.lift _ _ (fun _ _ ↦ .all _ _) (Coalgebra.comul x)) =
Algebra.TensorProduct.lift _ _ (fun _ _ ↦ .all _ _) (Coalgebra.comul x)
induction Coalgebra.comul (R := K) x with
| zero => simp only [map_zero]
| add x y _ _ => simp only [map_add, *]
| tmul x y => simp; rfl
smul_one r := by
ext x
change r (algebraMap _ _ _) = _
simp
rfl

These were added in #615

This PR removes two of them.

@kbuzzard
Copy link
Collaborator

Thanks!

@kbuzzard kbuzzard merged commit e514332 into ImperialCollegeLondon:main Feb 26, 2026
2 checks passed
@dwrensha dwrensha deleted the MulDistribMulAction-dedup branch February 26, 2026 17:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants