Skip to content

Commit bc87b03

Browse files
mattrobballmattrobball
committed
finish
1 parent 3426975 commit bc87b03

1 file changed

Lines changed: 71 additions & 28 deletions

File tree

‎Mathlib/Algebra/MonoidAlgebra/Basic.lean‎

Lines changed: 71 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1811,9 +1811,15 @@ theorem induction_on [AddMonoid G] {p : AddMonoidAlgebra k G → Prop} (f : AddM
18111811
@[simps]
18121812
def mapDomainRingHom (k : Type _) [Semiring k] {H F : Type _} [AddMonoid G] [AddMonoid H]
18131813
[AddMonoidHomClass F G H] (f : F) : AddMonoidAlgebra k G →+* AddMonoidAlgebra k H :=
1814-
{ (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra k G →+ MonoidAlgebra k H) with
1815-
map_one' := mapDomain_one f
1816-
map_mul' := fun x y => mapDomain_mul f x y }
1814+
{ toMonoidHom :=
1815+
{ toFun := (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra k G →+ MonoidAlgebra k H)
1816+
map_one' := mapDomain_one f
1817+
map_mul' := fun x y => mapDomain_mul f x y }
1818+
map_add' :=
1819+
(Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra k G →+ MonoidAlgebra k H).map_add'
1820+
map_zero' :=
1821+
(Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra k G →+ MonoidAlgebra k H).map_zero'
1822+
}
18171823
#align add_monoid_algebra.map_domain_ring_hom AddMonoidAlgebra.mapDomainRingHom
18181824
#align add_monoid_algebra.map_domain_ring_hom_apply AddMonoidAlgebra.mapDomainRingHom_apply
18191825

@@ -1835,9 +1841,13 @@ but for now we just construct the ring isomorphisms using `RingEquiv.refl _`.
18351841
`Multiplicative` -/
18361842
protected def AddMonoidAlgebra.toMultiplicative [Semiring k] [Add G] :
18371843
AddMonoidAlgebra k G ≃+* MonoidAlgebra k (Multiplicative G) :=
1838-
{ Finsupp.domCongr
1839-
Multiplicative.ofAdd with
1840-
toFun := equivMapDomain Multiplicative.ofAdd
1844+
{ toEquiv := {
1845+
toFun := equivMapDomain Multiplicative.ofAdd
1846+
invFun := Finsupp.domCongr Multiplicative.ofAdd|>.invFun
1847+
left_inv := Finsupp.domCongr Multiplicative.ofAdd|>.left_inv
1848+
right_inv := Finsupp.domCongr Multiplicative.ofAdd|>.right_inv}
1849+
map_add' := Finsupp.domCongr Multiplicative.ofAdd|>.map_add'
1850+
-- toFun := equivMapDomain Multiplicative.ofAdd
18411851
map_mul' := fun x y => by
18421852
-- Porting note: `dsimp` is required for beta reduction.
18431853
dsimp only []
@@ -1850,8 +1860,14 @@ protected def AddMonoidAlgebra.toMultiplicative [Semiring k] [Add G] :
18501860
/-- The equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of `Additive` -/
18511861
protected def MonoidAlgebra.toAdditive [Semiring k] [Mul G] :
18521862
MonoidAlgebra k G ≃+* AddMonoidAlgebra k (Additive G) :=
1853-
{ Finsupp.domCongr Additive.ofMul with
1854-
toFun := equivMapDomain Additive.ofMul
1863+
{ toEquiv := {
1864+
-- Finsupp.domCongr Additive.ofMul with
1865+
toFun := equivMapDomain Additive.ofMul
1866+
invFun := Finsupp.domCongr Additive.ofMul|>.invFun
1867+
left_inv := Finsupp.domCongr Additive.ofMul|>.left_inv
1868+
right_inv := Finsupp.domCongr Additive.ofMul|>.right_inv
1869+
}
1870+
map_add' := Finsupp.domCongr Additive.ofMul|>.map_add'
18551871
map_mul' := fun x y => by
18561872
-- Porting note: `dsimp` is required for beta reduction.
18571873
dsimp only []
@@ -1911,11 +1927,14 @@ direction. -/
19111927
@[simps apply_apply symm_apply]
19121928
def liftMagma [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] :
19131929
(Multiplicative G →ₙ* A) ≃ (AddMonoidAlgebra k G →ₙₐ[k] A) :=
1914-
{ (MonoidAlgebra.liftMagma k : (Multiplicative G →ₙ* A) ≃ (_ →ₙₐ[k] A)) with
1930+
{ --(MonoidAlgebra.liftMagma k : (Multiplicative G →ₙ* A) ≃ (_ →ₙₐ[k] A)) with
19151931
toFun := fun f =>
19161932
{ (MonoidAlgebra.liftMagma k f : _) with
19171933
toFun := fun a => sum a fun m t => t • f (Multiplicative.ofAdd m) }
1918-
invFun := fun F => F.toMulHom.comp (ofMagma k G) }
1934+
invFun := fun F => F.toMulHom.comp (ofMagma k G)
1935+
left_inv := (MonoidAlgebra.liftMagma k : (Multiplicative G →ₙ* A) ≃ (_ →ₙₐ[k] A)).left_inv
1936+
right_inv := (MonoidAlgebra.liftMagma k : (Multiplicative G →ₙ* A) ≃ (_ →ₙₐ[k] A)).right_inv
1937+
}
19191938
#align add_monoid_algebra.lift_magma AddMonoidAlgebra.liftMagma
19201939
#align add_monoid_algebra.lift_magma_apply_apply AddMonoidAlgebra.liftMagma_apply_apply
19211940
#align add_monoid_algebra.lift_magma_symm_apply AddMonoidAlgebra.liftMagma_symm_apply
@@ -1932,10 +1951,16 @@ section Algebra
19321951
/-- `Finsupp.single 0` as a `RingHom` -/
19331952
@[simps]
19341953
def singleZeroRingHom [Semiring k] [AddMonoid G] : k →+* AddMonoidAlgebra k G :=
1935-
{ Finsupp.singleAddHom 0 with
1936-
map_one' := rfl
1954+
{ toMonoidHom := {
1955+
toFun := Finsupp.singleAddHom 0
1956+
map_one' := rfl
1957+
map_mul' := fun x y => by simp [singleAddHom, single_mul_single, zero_add] }
1958+
map_add' := Finsupp.singleAddHom 0|>.map_add'
1959+
map_zero' := Finsupp.singleAddHom 0|>.map_zero'
1960+
}
1961+
-- map_one' := rfl
19371962
-- Porting note: Was `rw`.
1938-
map_mul' := fun x y => by simp only [singleAddHom, single_mul_single, zero_add] }
1963+
-- map_mul' := fun x y => by simp only [singleAddHom, single_mul_single, zero_add] }
19391964
#align add_monoid_algebra.single_zero_ring_hom AddMonoidAlgebra.singleZeroRingHom
19401965
#align add_monoid_algebra.single_zero_ring_hom_apply AddMonoidAlgebra.singleZeroRingHom_apply
19411966

@@ -1972,8 +1997,10 @@ the `AddMonoidAlgebra Rᵐᵒᵖ I` over the opposite ring, taking elements to t
19721997
@[simps! (config := { simpRhs := true }) apply symm_apply]
19731998
protected noncomputable def opRingEquiv [AddCommMonoid G] :
19741999
(AddMonoidAlgebra k G)ᵐᵒᵖ ≃+* AddMonoidAlgebra kᵐᵒᵖ G :=
1975-
{ MulOpposite.opAddEquiv.symm.trans
1976-
(Finsupp.mapRange.addEquiv (MulOpposite.opAddEquiv : k ≃+ kᵐᵒᵖ)) with
2000+
{ toEquiv := (MulOpposite.opAddEquiv.symm.trans
2001+
(Finsupp.mapRange.addEquiv (MulOpposite.opAddEquiv : k ≃+ kᵐᵒᵖ))).toEquiv
2002+
map_add' := (MulOpposite.opAddEquiv.symm.trans
2003+
(Finsupp.mapRange.addEquiv (MulOpposite.opAddEquiv : k ≃+ kᵐᵒᵖ))).map_add'
19772004
map_mul' := by
19782005
rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe, AddEquiv.coe_toEquiv,
19792006
← AddEquiv.coe_toAddMonoidHom]
@@ -2011,7 +2038,7 @@ In particular this provides the instance `Algebra k (AddMonoidAlgebra k G)`.
20112038
-/
20122039
instance algebra [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
20132040
Algebra R (AddMonoidAlgebra k G) :=
2014-
{ singleZeroRingHom.comp (algebraMap R k) with
2041+
{ toRingHom := singleZeroRingHom.comp (algebraMap R k)
20152042
-- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
20162043
smul_def' := fun r a => by
20172044
refine Finsupp.ext fun _ => ?_
@@ -2027,7 +2054,7 @@ instance algebra [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
20272054
@[simps! apply]
20282055
def singleZeroAlgHom [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
20292056
k →ₐ[R] AddMonoidAlgebra k G :=
2030-
{ singleZeroRingHom with
2057+
{ toRingHom := singleZeroRingHom
20312058
commutes' := fun r => by
20322059
-- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
20332060
refine Finsupp.ext fun _ => ?_
@@ -2053,10 +2080,10 @@ variable {A : Type u₃} [Semiring A] [Algebra k A] {B : Type _} [Semiring B] [A
20532080
/-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom` -/
20542081
def liftNCAlgHom (f : A →ₐ[k] B) (g : Multiplicative G →* B) (h_comm : ∀ x y, Commute (f x) (g y)) :
20552082
AddMonoidAlgebra A G →ₐ[k] B :=
2056-
{
2083+
{ toRingHom :=
20572084
liftNCRingHom (f : A →+* B) g
2058-
h_comm with
2059-
toFun := liftNCRingHom (f : A →+* B) g h_comm
2085+
h_comm
2086+
-- toFun := liftNCRingHom (f : A →+* B) g h_comm
20602087
commutes' := by simp [liftNCRingHom] }
20612088
#align add_monoid_algebra.lift_nc_alg_hom AddMonoidAlgebra.liftNCAlgHom
20622089

@@ -2082,11 +2109,13 @@ variable (k G A)
20822109
/-- Any monoid homomorphism `G →* A` can be lifted to an algebra homomorphism
20832110
`MonoidAlgebra k G →ₐ[k] A`. -/
20842111
def lift : (Multiplicative G →* A) ≃ (AddMonoidAlgebra k G →ₐ[k] A) :=
2085-
{ @MonoidAlgebra.lift k (Multiplicative G) _ _ A _ _ with
2112+
{ --@MonoidAlgebra.lift k (Multiplicative G) _ _ A _ _ with
20862113
invFun := fun f => (f : AddMonoidAlgebra k G →* A).comp (of k G)
20872114
toFun := fun F =>
20882115
{ @MonoidAlgebra.lift k (Multiplicative G) _ _ A _ _ F with
2089-
toFun := liftNCAlgHom (Algebra.ofId k A) F fun _ _ => Algebra.commutes _ _ } }
2116+
toFun := liftNCAlgHom (Algebra.ofId k A) F fun _ _ => Algebra.commutes _ _ }
2117+
left_inv := @MonoidAlgebra.lift k (Multiplicative G) _ _ A _ _ |>.left_inv
2118+
right_inv := @MonoidAlgebra.lift k (Multiplicative G) _ _ A _ _ |>.right_inv}
20902119
#align add_monoid_algebra.lift AddMonoidAlgebra.lift
20912120

20922121
variable {k G A}
@@ -2171,9 +2200,17 @@ non-unital algebra homomorphism between their additive magma algebras. -/
21712200
def mapDomainNonUnitalAlgHom (k A : Type _) [CommSemiring k] [Semiring A] [Algebra k A]
21722201
{G H F : Type _} [Add G] [Add H] [AddHomClass F G H] (f : F) :
21732202
AddMonoidAlgebra A G →ₙₐ[k] AddMonoidAlgebra A H :=
2174-
{ (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra A G →+ MonoidAlgebra A H) with
2175-
map_mul' := fun x y => mapDomain_mul f x y
2176-
map_smul' := fun r x => mapDomain_smul r x }
2203+
{ toDistribMulActionHom := {
2204+
toMulActionHom := {
2205+
toFun :=
2206+
(Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra A G →+ MonoidAlgebra A H)
2207+
map_smul' := fun r x => mapDomain_smul r x }
2208+
map_add' :=
2209+
(Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra A G →+ MonoidAlgebra A H).map_add'
2210+
map_zero' :=
2211+
(Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra A G →+ MonoidAlgebra A H).map_zero'
2212+
}
2213+
map_mul' := fun x y => mapDomain_mul f x y }
21772214
#align add_monoid_algebra.map_domain_non_unital_alg_hom AddMonoidAlgebra.mapDomainNonUnitalAlgHom
21782215
#align add_monoid_algebra.map_domain_non_unital_alg_hom_apply AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply
21792216

@@ -2183,7 +2220,7 @@ def mapDomainNonUnitalAlgHom (k A : Type _) [CommSemiring k] [Semiring A] [Algeb
21832220
def mapDomainAlgHom (k A : Type _) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G]
21842221
{H F : Type _} [AddMonoid H] [AddMonoidHomClass F G H] (f : F) :
21852222
AddMonoidAlgebra A G →ₐ[k] AddMonoidAlgebra A H :=
2186-
{ mapDomainRingHom A f with commutes' := mapDomain_algebraMap f }
2223+
{ toRingHom := mapDomainRingHom A f, commutes' := mapDomain_algebraMap f }
21872224
#align add_monoid_algebra.map_domain_alg_hom AddMonoidAlgebra.mapDomainAlgHom
21882225
#align add_monoid_algebra.map_domain_alg_hom_apply AddMonoidAlgebra.mapDomainAlgHom_apply
21892226

@@ -2195,13 +2232,19 @@ variable [CommSemiring R]
21952232
`Multiplicative`. -/
21962233
def AddMonoidAlgebra.toMultiplicativeAlgEquiv [Semiring k] [Algebra R k] [AddMonoid G] :
21972234
AddMonoidAlgebra k G ≃ₐ[R] MonoidAlgebra k (Multiplicative G) :=
2198-
{ AddMonoidAlgebra.toMultiplicative k G with
2235+
{ --AddMonoidAlgebra.toMultiplicative k G with
2236+
toEquiv := AddMonoidAlgebra.toMultiplicative k G|>.toEquiv
2237+
map_add' := AddMonoidAlgebra.toMultiplicative k G|>.map_add'
2238+
map_mul' := AddMonoidAlgebra.toMultiplicative k G|>.map_mul'
21992239
commutes' := fun r => by simp [AddMonoidAlgebra.toMultiplicative] }
22002240
#align add_monoid_algebra.to_multiplicative_alg_equiv AddMonoidAlgebra.toMultiplicativeAlgEquiv
22012241

22022242
/-- The algebra equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of
22032243
`Additive`. -/
22042244
def MonoidAlgebra.toAdditiveAlgEquiv [Semiring k] [Algebra R k] [Monoid G] :
22052245
MonoidAlgebra k G ≃ₐ[R] AddMonoidAlgebra k (Additive G) :=
2206-
{ MonoidAlgebra.toAdditive k G with commutes' := fun r => by simp [MonoidAlgebra.toAdditive] }
2246+
{ toEquiv := MonoidAlgebra.toAdditive k G|>.toEquiv
2247+
map_add' := MonoidAlgebra.toAdditive k G|>.map_add'
2248+
map_mul' := MonoidAlgebra.toAdditive k G|>.map_mul'
2249+
commutes' := fun r => by simp [MonoidAlgebra.toAdditive] }
22072250
#align monoid_algebra.to_additive_alg_equiv MonoidAlgebra.toAdditiveAlgEquiv

0 commit comments

Comments
 (0)