forked from leanprover-community/mathlib
-
Notifications
You must be signed in to change notification settings - Fork 0
/
conj.lean
142 lines (102 loc) · 5.72 KB
/
conj.lean
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) 2019 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import category_theory.isomorphism data.equiv.basic category_theory.endomorphism algebra.group_power
/-!
# Conjugate morphisms by isomorphisms
An isomorphism `α : X ≅ Y` defines
- a monoid isomorphism `conj : End X ≃* End Y` by `α.conj f = α.inv ≫ f ≫ α.hom`;
- a group isomorphism `conj_Aut : Aut X ≃* Aut Y` by `α.conj_Aut f = α.symm ≪≫ f ≪≫ α`.
For completeness, we also define `hom_congr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁)`, cf. `equiv.arrow_congr`.
-/
universes v u
namespace category_theory
namespace iso
variables {C : Type u} [𝒞 : category.{v} C]
include 𝒞
/- If `X` is isomorphic to `X₁` and `Y` is isomorphic to `Y₁`, then
there is a natural bijection between `X ⟶ Y` and `X₁ ⟶ Y₁`. See also `equiv.arrow_congr`. -/
def hom_congr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) :
(X ⟶ Y) ≃ (X₁ ⟶ Y₁) :=
{ to_fun := λ f, α.inv ≫ f ≫ β.hom,
inv_fun := λ f, α.hom ≫ f ≫ β.inv,
left_inv := λ f, show α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f,
by rw [category.assoc, category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, category.comp_id],
right_inv := λ f, show α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f,
by rw [category.assoc, category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, category.comp_id] }
lemma hom_congr_apply {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) :
α.hom_congr β f = α.inv ≫ f ≫ β.hom :=
rfl
lemma hom_congr_comp {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁)
(f : X ⟶ Y) (g : Y ⟶ Z) :
α.hom_congr γ (f ≫ g) = (α.hom_congr β f) ≫ (hom_congr β γ g) :=
by simp only [hom_congr_apply, category.assoc, β.hom_inv_id_assoc]
@[simp] lemma hom_congr_refl {X Y : C} (f : X ⟶ Y) :
(iso.refl X).hom_congr (iso.refl Y) f = f :=
by simp only [hom_congr_apply, iso.refl, category.comp_id, category.id_comp]
@[simp] lemma hom_congr_trans {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C}
(α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃) (f : X₁ ⟶ Y₁) :
(α₁ ≪≫ α₂).hom_congr (β₁ ≪≫ β₂) f = (α₁.hom_congr β₁).trans (α₂.hom_congr β₂) f :=
by simp only [hom_congr_apply, equiv.trans_apply, iso.trans, category.assoc]
@[simp] lemma hom_congr_symm {X₁ Y₁ X₂ Y₂ : C} (α : X₁ ≅ X₂) (β : Y₁ ≅ Y₂) :
(α.hom_congr β).symm = α.symm.hom_congr β.symm :=
rfl
variables {X Y : C} (α : X ≅ Y)
/-- An isomorphism between two objects defines a monoid isomorphism between their
monoid of endomorphisms. -/
def conj : End X ≃* End Y :=
{ map_mul' := λ f g, hom_congr_comp α α α g f,
.. hom_congr α α }
lemma conj_apply (f : End X) : α.conj f = α.inv ≫ f ≫ α.hom := rfl
@[simp] lemma conj_comp (f g : End X) : α.conj (f ≫ g) = (α.conj f) ≫ (α.conj g) :=
is_mul_hom.map_mul α.conj g f
@[simp] lemma conj_id : α.conj (𝟙 X) = 𝟙 Y :=
is_monoid_hom.map_one α.conj
@[simp] lemma refl_conj (f : End X) : (@iso.refl C 𝒞 X).conj f = f :=
by rw [conj_apply, iso.refl_inv, iso.refl_hom, category.id_comp, category.comp_id]
@[simp] lemma trans_conj {Z : C} (β : Y ≅ Z) (f : End X) : (α ≪≫ β).conj f = β.conj (α.conj f) :=
hom_congr_trans α α β β f
@[simp] lemma symm_self_conj (f : End X) : α.symm.conj (α.conj f) = f :=
by rw [← trans_conj, α.self_symm_id, refl_conj]
@[simp] lemma self_symm_conj (f : End Y) : α.conj (α.symm.conj f) = f :=
α.symm.symm_self_conj f
@[simp] lemma conj_pow (f : End X) (n : ℕ) : α.conj (f^n) = (α.conj f)^n :=
is_monoid_hom.map_pow α.conj f n
/-- `conj` defines a group isomorphisms between groups of automorphisms -/
def conj_Aut : Aut X ≃* Aut Y :=
(Aut.units_End_equiv_Aut X).symm.trans $
(units.map_equiv α.conj).trans $
Aut.units_End_equiv_Aut Y
lemma conj_Aut_apply (f : Aut X) : α.conj_Aut f = α.symm ≪≫ f ≪≫ α :=
by cases f; cases α; ext; refl
@[simp] lemma conj_Aut_hom (f : Aut X) : (α.conj_Aut f).hom = α.conj f.hom := rfl
@[simp] lemma trans_conj_Aut {Z : C} (β : Y ≅ Z) (f : Aut X) :
(α ≪≫ β).conj_Aut f = β.conj_Aut (α.conj_Aut f) :=
by simp only [conj_Aut_apply, iso.trans_symm, iso.trans_assoc]
@[simp] lemma conj_Aut_mul (f g : Aut X) : α.conj_Aut (f * g) = α.conj_Aut f * α.conj_Aut g :=
is_mul_hom.map_mul α.conj_Aut f g
@[simp] lemma conj_Aut_trans (f g : Aut X) : α.conj_Aut (f ≪≫ g) = α.conj_Aut f ≪≫ α.conj_Aut g :=
conj_Aut_mul α g f
@[simp] lemma conj_Aut_pow (f : Aut X) (n : ℕ) : α.conj_Aut (f^n) = (α.conj_Aut f)^n :=
is_monoid_hom.map_pow α.conj_Aut f n
@[simp] lemma conj_Aut_gpow (f : Aut X) (n : ℤ) : α.conj_Aut (f^n) = (α.conj_Aut f)^n :=
is_group_hom.map_gpow α.conj_Aut f n
end iso
namespace functor
universes v₁ u₁
variables {C : Type u} [𝒞 : category.{v} C] {D : Type u₁} [𝒟 : category.{v₁} D] (F : C ⥤ D)
include 𝒞 𝒟
lemma map_hom_congr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) :
F.map (iso.hom_congr α β f) = iso.hom_congr (F.map_iso α) (F.map_iso β) (F.map f) :=
by simp only [iso.hom_congr_apply, F.map_comp, F.map_iso_inv, F.map_iso_hom]
lemma map_conj {X Y : C} (α : X ≅ Y) (f : End X) :
F.map (α.conj f) = (F.map_iso α).conj (F.map f) :=
map_hom_congr F α α f
lemma map_conj_Aut (F : C ⥤ D) {X Y : C} (α : X ≅ Y) (f : Aut X) :
F.map_iso (α.conj_Aut f) = (F.map_iso α).conj_Aut (F.map_iso f) :=
by ext; simp only [map_iso_hom, iso.conj_Aut_hom, F.map_conj]
-- alternative proof: by simp only [iso.conj_Aut_apply, F.map_iso_trans, F.map_iso_symm]
end functor
end category_theory