feat(algebra/category/Algebra): basic setup for category of bundled R…

…-algebras (#3047)

Just boilerplate. If I don't run out of enthusiasm I'll do tensor product of R-algebras soon. (#3050)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/category/Algebra/basic.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import algebra.category.CommRing.basic
+import algebra.category.Module.basic
+import ring_theory.algebra
+
+open category_theory
+open category_theory.limits
+
+universe u
+
+variables (R : Type u) [comm_ring R]
+
+/-- The category of R-modules and their morphisms. -/
+structure Algebra :=
+(carrier : Type u)
+[is_ring : ring carrier]
+[is_algebra : algebra R carrier]
+
+attribute [instance] Algebra.is_ring Algebra.is_algebra
+
+namespace Algebra
+
+instance : has_coe_to_sort (Algebra R) :=
+{ S := Type u, coe := Algebra.carrier }
+
+instance : category (Algebra.{u} R) :=
+{ hom   := λ A B, A →ₐ[R] B,
+  id    := λ A, alg_hom.id R A,
+  comp  := λ A B C f g, g.comp f }
+
+instance : concrete_category (Algebra.{u} R) :=
+{ forget := { obj := λ R, R, map := λ R S f, (f : R → S) },
+  forget_faithful := { } }
+
+instance has_forget_to_Ring : has_forget₂ (Algebra R) Ring :=
+{ forget₂ :=
+  { obj := λ A, Ring.of A,
+    map := λ A₁ A₂ f, alg_hom.to_ring_hom f, } }
+
+instance has_forget_to_Module : has_forget₂ (Algebra R) (Module R) :=
+{ forget₂ :=
+  { obj := λ M, Module.of R M,
+    map := λ M₁ M₂ f, alg_hom.to_linear_map f, } }
+
+/-- The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. -/
+def of (X : Type u) [ring X] [algebra R X] : Algebra R := ⟨X⟩
+
+instance : inhabited (Algebra R) := ⟨of R R⟩
+
+@[simp]
+lemma of_apply (X : Type u) [ring X] [algebra R X] :
+  (of R X : Type u) = X := rfl
+
+variables {R}
+
+/-- Forgetting to the underlying type and then building the bundled object returns the original algebra. -/
+@[simps]
+def of_self_iso (M : Algebra R) : Algebra.of R M ≅ M :=
+{ hom := 𝟙 M, inv := 𝟙 M }
+
+variables {R} {M N U : Module R}
+
+@[simp] lemma id_apply (m : M) : (𝟙 M : M → M) m = m := rfl
+
+@[simp] lemma coe_comp (f : M ⟶ N) (g : N ⟶ U) :
+  ((f ≫ g) : M → U) = g ∘ f := rfl
+
+end Algebra
+
+variables {R}
+variables {X₁ X₂ : Type u}
+
+/-- Build an isomorphism in the category `Algebra R` from a `alg_equiv` between `algebra`s. -/
+@[simps]
+def alg_equiv.to_Algebra_iso
+  {g₁ : ring X₁} {g₂ : ring X₂} {m₁ : algebra R X₁} {m₂ : algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :
+  Algebra.of R X₁ ≅ Algebra.of R X₂ :=
+{ hom := (e : X₁ →ₐ[R] X₂),
+  inv := (e.symm : X₂ →ₐ[R] X₁),
+  hom_inv_id' := begin ext, exact e.left_inv x, end,
+  inv_hom_id' := begin ext, exact e.right_inv x, end, }
+
+namespace category_theory.iso
+
+/-- Build a `alg_equiv` from an isomorphism in the category `Algebra R`. -/
+@[simps]
+def to_alg_equiv {X Y : Algebra.{u} R} (i : X ≅ Y) : X ≃ₐ[R] Y :=
+{ to_fun    := i.hom,
+  inv_fun   := i.inv,
+  left_inv  := by tidy,
+  right_inv := by tidy,
+  map_add'  := by tidy,
+  map_mul'  := by tidy,
+  commutes' := by tidy, }.
+
+end category_theory.iso
+
+/-- algebra equivalences between `algebras`s are the same as (isomorphic to) isomorphisms in `Algebra` -/
+@[simps]
+def alg_equiv_iso_Algebra_iso {X Y : Type u}
+  [ring X] [ring Y] [algebra R X] [algebra R Y] :
+  (X ≃ₐ[R] Y) ≅ (Algebra.of R X ≅ Algebra.of R Y) :=
+{ hom := λ e, e.to_Algebra_iso,
+  inv := λ i, i.to_alg_equiv, }
+
+instance (X : Type u) [ring X] [algebra R X] : has_coe (subalgebra R X) (Algebra R) :=
+⟨ λ N, Algebra.of R N ⟩

src/algebra/category/Module/basic.lean

@@ -112,7 +112,7 @@ end category_theory.iso
 
 /-- linear equivalences between `module`s are the same as (isomorphic to) isomorphisms in `Module` -/
 @[simps]
-def linear_equiv_iso_Group_iso {X Y : Type u} [add_comm_group X] [add_comm_group Y] [module R X] [module R Y] :
+def linear_equiv_iso_Module_iso {X Y : Type u} [add_comm_group X] [add_comm_group Y] [module R X] [module R Y] :
   (X ≃ₗ[R] Y) ≅ (Module.of R X ≅ Module.of R Y) :=
 { hom := λ e, e.to_Module_iso,
   inv := λ i, i.to_linear_equiv, }

src/ring_theory/algebra.lean

@@ -241,6 +241,7 @@ coe_fn_inj $ funext H
 theorem ext_iff {φ₁ φ₂ : A →ₐ[R] B} : φ₁ = φ₂ ↔ ∀ x, φ₁ x = φ₂ x :=
 ⟨by { rintro rfl x, refl }, ext⟩
 
+@[simp]
 theorem commutes (r : R) : φ (algebra_map R A r) = algebra_map R B r := φ.commutes' r
 
 theorem comp_algebra_map : φ.to_ring_hom.comp (algebra_map R A) = algebra_map R B :=
@@ -360,6 +361,22 @@ variables [algebra R A₁] [algebra R A₂] [algebra R A₃]
 
 instance : has_coe_to_fun (A₁ ≃ₐ[R] A₂) := ⟨_, alg_equiv.to_fun⟩
 
+@[ext]
+lemma ext {f g : A₁ ≃ₐ[R] A₂} (h : ∀ a, f a = g a) : f = g :=
+begin
+  have h₁ : f.to_equiv = g.to_equiv := equiv.ext h,
+  cases f, cases g, congr,
+  { exact (funext h) },
+  { exact congr_arg equiv.inv_fun h₁ }
+end
+
+lemma coe_fun_injective : @function.injective (A₁ ≃ₐ[R] A₂) (A₁ → A₂) (λ e, (e : A₁ → A₂)) :=
+begin
+  intros f g w,
+  ext,
+  exact congr_fun w a,
+end
+
 instance has_coe_to_ring_equiv : has_coe (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂) := ⟨alg_equiv.to_ring_equiv⟩
 
 @[simp] lemma mk_apply {to_fun inv_fun left_inv right_inv map_mul map_add commutes a} :
@@ -370,6 +387,15 @@ rfl
 
 @[simp, norm_cast] lemma coe_ring_equiv (e : A₁ ≃ₐ[R] A₂) : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e := rfl
 
+lemma coe_ring_equiv_injective : function.injective (λ e : A₁ ≃ₐ[R] A₂, (e : A₁ ≃+* A₂)) :=
+begin
+  intros f g w,
+  ext,
+  replace w : ((f : A₁ ≃+* A₂) : A₁ → A₂) = ((g : A₁ ≃+* A₂) : A₁ → A₂) :=
+    congr_arg (λ e : A₁ ≃+* A₂, (e : A₁ → A₂)) w,
+  exact congr_fun w a,
+end
+
 @[simp] lemma map_add (e : A₁ ≃ₐ[R] A₂) : ∀ x y, e (x + y) = e x + e y := e.to_add_equiv.map_add
 
 @[simp] lemma map_zero (e : A₁ ≃ₐ[R] A₂) : e 0 = 0 := e.to_add_equiv.map_zero