-
Notifications
You must be signed in to change notification settings - Fork 1.2k
Expand file tree
/
Copy pathCentroidHom.lean
More file actions
142 lines (112 loc) · 5.51 KB
/
CentroidHom.lean
File metadata and controls
142 lines (112 loc) · 5.51 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
/-
Copyright (c) 2024 Christopher Hoskin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christopher Hoskin
-/
module
public import Mathlib.Algebra.Ring.CentroidHom
public import Mathlib.Algebra.Star.StarRingHom
public import Mathlib.Algebra.Star.Subsemiring
public import Mathlib.Algebra.Star.Basic
/-!
# Centroid homomorphisms on Star Rings
When a (nonunital, non-associative) semiring is equipped with an involutive automorphism the
center of the centroid becomes a star ring in a natural way and the natural mapping of the centre of
the semiring into the centre of the centroid becomes a *-homomorphism.
## Tags
centroid
-/
@[expose] public section
variable {α : Type*}
namespace CentroidHom
section NonUnitalNonAssocStarSemiring
variable [NonUnitalNonAssocSemiring α] [StarRing α]
instance : Star (CentroidHom α) where
star f :=
{ toFun := fun a => star (f (star a))
map_zero' := by
simp only [star_zero, map_zero]
map_add' := fun a b => by simp only [star_add, map_add]
map_mul_left' := fun a b => by simp only [star_mul, map_mul_right, star_star]
map_mul_right' := fun a b => by simp only [star_mul, map_mul_left, star_star] }
@[simp] lemma star_apply (f : CentroidHom α) (a : α) : (star f) a = star (f (star a)) := rfl
instance instStarAddMonoid : StarAddMonoid (CentroidHom α) where
star_involutive f := ext (fun _ => by
rw [star_apply, star_apply, star_star, star_star])
star_add _ _ := ext fun _ => star_add _ _
instance : Star (Subsemiring.center (CentroidHom α)) where
star f := ⟨star (f : CentroidHom α), Subsemiring.mem_center_iff.mpr (fun g => ext (fun a =>
calc
g (star (f (star a))) = star (star g (f (star a))) := by rw [star_apply, star_star]
_ = star ((star g * f) (star a)) := rfl
_ = star ((f * star g) (star a)) := by rw [f.property.comm]
_ = star (f (star g (star a))) := rfl
_ = star (f (star (g a))) := by rw [star_apply, star_star]))⟩
instance instStarAddMonoidCenter : StarAddMonoid (Subsemiring.center (CentroidHom α)) where
star_involutive f := SetCoe.ext (star_involutive f.val)
star_add f g := SetCoe.ext (star_add f.val g.val)
set_option backward.isDefEq.respectTransparency false in
instance : StarRing (Subsemiring.center (CentroidHom α)) where
__ := instStarAddMonoidCenter
star_mul f g := by
ext a
calc
star (f * g) a = star (g * f) a := by rw [CommMonoid.mul_comm f g]
_ = star (g (f (star a))) := rfl
_ = star (g (star (star (f (star a))))) := by simp only [star_star]
_ = (star g * star f) a := rfl
/-- The canonical *-homomorphism embedding the center of `CentroidHom α` into `CentroidHom α`. -/
def centerStarEmbedding : Subsemiring.center (CentroidHom α) →⋆ₙ+* CentroidHom α where
toNonUnitalRingHom :=
(SubsemiringClass.subtype (Subsemiring.center (CentroidHom α))).toNonUnitalRingHom
map_star' _ := rfl
theorem star_centerToCentroidCenter (z : NonUnitalStarSubsemiring.center α) :
star (centerToCentroidCenter z) =
(centerToCentroidCenter (star z : NonUnitalStarSubsemiring.center α)) := by
ext a
calc
(star (centerToCentroidCenter z)) a = star (z * star a) := rfl
_ = star (star a) * star z := by simp only [star_mul, star_star, StarMemClass.coe_star]
_ = a * star z := by rw [star_star]
_ = (star z) * a := by rw [(star z).property.comm]
_ = (centerToCentroidCenter ((star z) : NonUnitalStarSubsemiring.center α)) a := rfl
/-- The canonical *-homomorphism from the center of a non-unital, non-associative *-semiring into
the center of its centroid. -/
def starCenterToCentroidCenter :
NonUnitalStarSubsemiring.center α →⋆ₙ+* Subsemiring.center (CentroidHom α) where
toNonUnitalRingHom := centerToCentroidCenter
map_star' _ := (star_centerToCentroidCenter _).symm
/-- The canonical homomorphism from the center into the centroid -/
def starCenterToCentroid : NonUnitalStarSubsemiring.center α →⋆ₙ+* CentroidHom α :=
NonUnitalStarRingHom.comp (centerStarEmbedding) (starCenterToCentroidCenter)
lemma starCenterToCentroid_apply (z : NonUnitalStarSubsemiring.center α) (a : α) :
(starCenterToCentroid z) a = z * a := rfl
/--
Let `α` be a star ring with commutative centroid. Then the centroid is a star ring.
-/
@[reducible]
def starRingOfCommCentroidHom (mul_comm : IsMulCommutative (CentroidHom α)) :
StarRing (CentroidHom α) where
__ := instStarAddMonoid
star_mul _ _ := ext fun _ ↦ by simp [mul_comm']
end NonUnitalNonAssocStarSemiring
section NonAssocStarSemiring
variable [NonAssocSemiring α] [StarRing α]
/-- The canonical isomorphism from the center of a (non-associative) semiring onto its centroid. -/
def starCenterIsoCentroid : StarSubsemiring.center α ≃⋆+* CentroidHom α where
__ := starCenterToCentroid
invFun T :=
⟨T 1, by constructor <;> simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]⟩
left_inv z := Subtype.ext <| by simp only [MulHom.toFun_eq_coe,
NonUnitalRingHom.coe_toMulHom, NonUnitalStarRingHom.coe_toNonUnitalRingHom,
starCenterToCentroid_apply, mul_one]
right_inv T := CentroidHom.ext <| fun _ => by
simp [starCenterToCentroid_apply, ← map_mul_right]
@[simp]
lemma starCenterIsoCentroid_apply (a : ↥(NonUnitalStarSubsemiring.center α)) :
CentroidHom.starCenterIsoCentroid a = CentroidHom.starCenterToCentroid a := rfl
@[simp]
lemma starCenterIsoCentroid_symm_apply_coe (T : CentroidHom α) :
↑(CentroidHom.starCenterIsoCentroid.symm T) = T 1 := rfl
end NonAssocStarSemiring
end CentroidHom