chore(algebra/free_algebra): Make the second type argument to lift an…

…d ι implicit (#4299)

These can always be inferred by the context, and just make things longer.
This is consistent with how the type argument for `id` is implicit.

The changes are applied to downstream uses too.

src/algebra/free_algebra.lean

@@ -16,15 +16,15 @@ Given a commutative semiring `R`, and a type `X`, we construct the free `R`-alge
 ## Notation
 
 1. `free_algebra R X` is the free algebra itself. It is endowed with an `R`-algebra structure.
-2. `free_algebra.ι R X` is the function `X → free_algebra R X`.
-3. Given a function `f : X → A` to an R-algebra `A`, `lift R X f` is the lift of `f` to an
+2. `free_algebra.ι R` is the function `X → free_algebra R X`.
+3. Given a function `f : X → A` to an R-algebra `A`, `lift R f` is the lift of `f` to an
   `R`-algebra morphism `free_algebra R X → A`.
 
 ## Theorems
 
-1. `ι_comp_lift` states that the composition `(lift R X f) ∘ (ι R X)` is identical to `f`.
+1. `ι_comp_lift` states that the composition `(lift R f) ∘ (ι R)` is identical to `f`.
 2. `lift_unique` states that whenever an R-algebra morphism `g : free_algebra R X → A` is
-  given whose composition with `ι R X` is `f`, then one has `g = lift R X f`.
+  given whose composition with `ι R` is `f`, then one has `g = lift R f`.
 3. `hom_ext` is a variant of `lift_unique` in the form of an extensionality theorem.
 4. `lift_comp_ι` is a combination of `ι_comp_lift` and `lift_unique`. It states that the lift
   of the composition of an algebra morphism with `ι` is the algebra morphism itself.
@@ -173,15 +173,17 @@ instance : algebra R (free_algebra R X) :=
   commutes' := λ _, by { rintros ⟨⟩, exact quot.sound rel.central_scalar },
   smul_def' := λ _ _, rfl }
 
+variables {X}
+
 /--
 The canonical function `X → free_algebra R X`.
 -/
 def ι : X → free_algebra R X := λ m, quot.mk _ m
 
-@[simp] lemma quot_mk_eq_ι (m : X) : quot.mk (free_algebra.rel R X) m = ι R X m := rfl
+@[simp] lemma quot_mk_eq_ι (m : X) : quot.mk (free_algebra.rel R X) m = ι R m := rfl
 
 /--
-Given a function `f : X → A` where `A` is an `R`-algebra, `lift R X f` is the unique lift
+Given a function `f : X → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
 of `f` to a morphism of `R`-algebras `free_algebra R X → A`.
 -/
 def lift {A : Type*} [semiring A] [algebra R A] (f : X → A) : free_algebra R X →ₐ[R] A :=
@@ -228,22 +230,22 @@ variables {R X}
 
 @[simp]
 theorem ι_comp_lift {A : Type*} [semiring A] [algebra R A] (f : X → A) :
-  (lift R X f : free_algebra R X → A) ∘ (ι R X) = f := by {ext, refl}
+  (lift R f : free_algebra R X → A) ∘ (ι R) = f := by {ext, refl}
 
 @[simp]
 theorem lift_ι_apply {A : Type*} [semiring A] [algebra R A] (f : X → A) (x) :
-  lift R X f (ι R X x) = f x := rfl
+  lift R f (ι R x) = f x := rfl
 
 @[simp]
 theorem lift_unique {A : Type*} [semiring A] [algebra R A] (f : X → A)
   (g : free_algebra R X →ₐ[R] A) :
-  (g : free_algebra R X → A) ∘ (ι R X) = f ↔ g = lift R X f :=
+  (g : free_algebra R X → A) ∘ (ι R) = f ↔ g = lift R f :=
 begin
   refine ⟨λ hyp, _, λ hyp, by rw [hyp, ι_comp_lift]⟩,
   ext,
   rcases x,
   induction x,
-  { change ((g : free_algebra R X → A) ∘ (ι R X)) _ = _,
+  { change ((g : free_algebra R X → A) ∘ (ι R)) _ = _,
     rw hyp,
     refl },
   { exact alg_hom.commutes g x },
@@ -264,13 +266,13 @@ attribute [irreducible] free_algebra ι lift
 
 @[simp]
 theorem lift_comp_ι {A : Type*} [semiring A] [algebra R A] (g : free_algebra R X →ₐ[R] A) :
-  lift R X ((g : free_algebra R X → A) ∘ (ι R X)) = g := by {symmetry, rw ←lift_unique}
+  lift R ((g : free_algebra R X → A) ∘ (ι R)) = g := by {symmetry, rw ←lift_unique}
 
 @[ext]
 theorem hom_ext {A : Type*} [semiring A] [algebra R A] {f g : free_algebra R X →ₐ[R] A}
-  (w : ((f : free_algebra R X → A) ∘ (ι R X)) = ((g : free_algebra R X → A) ∘ (ι R X))) : f = g :=
+  (w : ((f : free_algebra R X → A) ∘ (ι R)) = ((g : free_algebra R X → A) ∘ (ι R))) : f = g :=
 begin
-  have : g = lift R X ((g : free_algebra R X → A) ∘ (ι R X)), by rw ←lift_unique,
+  have : g = lift R ((g : free_algebra R X → A) ∘ (ι R)), by rw ←lift_unique,
   rw [this, ←lift_unique, w],
 end
 
@@ -283,8 +285,8 @@ for example.
 noncomputable
 def equiv_monoid_algebra_free_monoid : free_algebra R X ≃ₐ[R] monoid_algebra R (free_monoid X) :=
 alg_equiv.of_alg_hom
-  (lift R X (λ x, (monoid_algebra.of R (free_monoid X)) (free_monoid.of x)))
-  ((monoid_algebra.lift R (free_monoid X) (free_algebra R X)) (free_monoid.lift (ι R X)))
+  (lift R (λ x, (monoid_algebra.of R (free_monoid X)) (free_monoid.of x)))
+  ((monoid_algebra.lift R (free_monoid X) (free_algebra R X)) (free_monoid.lift (ι R)))
 begin
   apply monoid_algebra.alg_hom_ext, intro x,
   apply free_monoid.rec_on x,

src/algebra/lie/universal_enveloping.lean

@@ -38,7 +38,7 @@ universes u₁ u₂ u₃
 variables (R : Type u₁) (L : Type u₂)
 variables [comm_ring R] [lie_ring L] [lie_algebra R L]
 
-local notation `ιₜ` := tensor_algebra.ι R L
+local notation `ιₜ` := tensor_algebra.ι R
 
 namespace universal_enveloping_algebra
 
@@ -65,6 +65,8 @@ associative algebras. -/
 def mk_alg_hom : tensor_algebra R L →ₐ[R] universal_enveloping_algebra R L :=
 ring_quot.mk_alg_hom R (rel R L)
 
+variables {L}
+
 /-- The natural Lie algebra morphism from a Lie algebra to its universal enveloping algebra. -/
 def ι : L →ₗ⁅R⁆ universal_enveloping_algebra R L :=
 { map_lie   := λ x y, by
@@ -78,23 +80,23 @@ variables {A : Type u₃} [ring A] [algebra R A] (f : L →ₗ⁅R⁆ A)
 /-- The universal property of the universal enveloping algebra: Lie algebra morphisms into
 associative algebras lift to associative algebra morphisms from the universal enveloping algebra. -/
 def lift : universal_enveloping_algebra R L →ₐ[R] A :=
-ring_quot.lift_alg_hom R (tensor_algebra.lift R L (f : L →ₗ[R] A))
+ring_quot.lift_alg_hom R (tensor_algebra.lift R (f : L →ₗ[R] A))
 begin
   intros a b h, induction h with x y,
   simp [lie_ring.of_associative_ring_bracket],
 end
 
-@[simp] lemma lift_ι_apply (x : L) : lift R L f (ι R L x) = f x :=
+@[simp] lemma lift_ι_apply (x : L) : lift R f (ι R x) = f x :=
 begin
-  have : ι R L x = ring_quot.mk_alg_hom R (rel R L) (ιₜ x), by refl,
+  have : ι R x = ring_quot.mk_alg_hom R (rel R L) (ιₜ x), by refl,
   simp [this, lift],
 end
 
-lemma ι_comp_lift : (lift R L f) ∘ (ι R L) = f :=
+lemma ι_comp_lift : (lift R f) ∘ (ι R) = f :=
 by { ext, simp, }
 
 lemma lift_unique (g : universal_enveloping_algebra R L →ₐ[R] A) :
-  g ∘ (ι R L) = f ↔ g = lift R L f :=
+  g ∘ (ι R) = f ↔ g = lift R f :=
 begin
   split; intros h,
   { apply ring_quot.lift_alg_hom_unique,
@@ -106,13 +108,13 @@ begin
 end
 
 @[ext] lemma hom_ext {g₁ g₂ : universal_enveloping_algebra R L →ₐ[R] A}
-  (h : g₁ ∘ (ι R L) = g₂ ∘ (ι R L)) : g₁ = g₂ :=
+  (h : g₁ ∘ (ι R) = g₂ ∘ (ι R)) : g₁ = g₂ :=
 begin
-  let f₁ := (lie_algebra.of_associative_algebra_hom g₁).comp (ι R L),
-  let f₂ := (lie_algebra.of_associative_algebra_hom g₂).comp (ι R L),
+  let f₁ := (lie_algebra.of_associative_algebra_hom g₁).comp (ι R),
+  let f₂ := (lie_algebra.of_associative_algebra_hom g₂).comp (ι R),
   have h' : f₁ = f₂, { ext, exact congr h rfl, },
-  have h₁ : g₁ = lift R L f₁, { rw ← lift_unique, refl, },
-  have h₂ : g₂ = lift R L f₂, { rw ← lift_unique, refl, },
+  have h₁ : g₁ = lift R f₁, { rw ← lift_unique, refl, },
+  have h₂ : g₂ = lift R f₂, { rw ← lift_unique, refl, },
   rw [h₁, h₂, h'],
 end
 

src/linear_algebra/tensor_algebra.lean

@@ -15,15 +15,15 @@ This is the free `R`-algebra generated (`R`-linearly) by the module `M`.
 ## Notation
 
 1. `tensor_algebra R M` is the tensor algebra itself. It is endowed with an R-algebra structure.
-2. `tensor_algebra.ι R M` is the canonical R-linear map `M → tensor_algebra R M`.
-3. Given a linear map `f : M → A` to an R-algebra `A`, `lift R M f` is the lift of `f` to an
+2. `tensor_algebra.ι R` is the canonical R-linear map `M → tensor_algebra R M`.
+3. Given a linear map `f : M → A` to an R-algebra `A`, `lift R f` is the lift of `f` to an
   `R`-algebra morphism `tensor_algebra R M → A`.
 
 ## Theorems
 
-1. `ι_comp_lift` states that the composition `(lift R M f) ∘ (ι R M)` is identical to `f`.
+1. `ι_comp_lift` states that the composition `(lift R f) ∘ (ι R)` is identical to `f`.
 2. `lift_unique` states that whenever an R-algebra morphism `g : tensor_algebra R M → A` is
-  given whose composition with `ι R M` is `f`, then one has `g = lift R M f`.
+  given whose composition with `ι R` is `f`, then one has `g = lift R f`.
 3. `hom_ext` is a variant of `lift_unique` in the form of an extensionality theorem.
 4. `lift_comp_ι` is a combination of `ι_comp_lift` and `lift_unique`. It states that the lift
   of the composition of an algebra morphism with `ι` is the algebra morphism itself.
@@ -46,9 +46,9 @@ the associated quotient.
 inductive rel : free_algebra R M → free_algebra R M → Prop
 -- force `ι` to be linear
 | add {a b : M} :
-  rel (free_algebra.ι R M (a+b)) (free_algebra.ι R M a + free_algebra.ι R M b)
+  rel (free_algebra.ι R (a+b)) (free_algebra.ι R a + free_algebra.ι R b)
 | smul {r : R} {a : M} :
-  rel (free_algebra.ι R M (r • a)) (algebra_map R (free_algebra R M) r * free_algebra.ι R M a)
+  rel (free_algebra.ι R (r • a)) (algebra_map R (free_algebra R M) r * free_algebra.ι R a)
 
 end tensor_algebra
 
@@ -60,37 +60,38 @@ def tensor_algebra := ring_quot (tensor_algebra.rel R M)
 
 namespace tensor_algebra
 
+variables {M}
 /--
 The canonical linear map `M →ₗ[R] tensor_algebra R M`.
 -/
 def ι : M →ₗ[R] (tensor_algebra R M) :=
-{ to_fun := λ m, (ring_quot.mk_alg_hom R _ (free_algebra.ι R M m)),
+{ to_fun := λ m, (ring_quot.mk_alg_hom R _ (free_algebra.ι R m)),
   map_add' := λ x y, by { rw [←alg_hom.map_add], exact ring_quot.mk_alg_hom_rel R rel.add, },
   map_smul' := λ r x, by { rw [←alg_hom.map_smul], exact ring_quot.mk_alg_hom_rel R rel.smul, } }
 
 lemma ring_quot_mk_alg_hom_free_algebra_ι_eq_ι (m : M) :
-  ring_quot.mk_alg_hom R (rel R M) (free_algebra.ι R M m) = ι R M m := rfl
+  ring_quot.mk_alg_hom R (rel R M) (free_algebra.ι R m) = ι R m := rfl
 
 /--
-Given a linear map `f : M → A` where `A` is an `R`-algebra, `lift R M f` is the unique lift
+Given a linear map `f : M → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
 of `f` to a morphism of `R`-algebras `tensor_algebra R M → A`.
 -/
 def lift {A : Type*} [semiring A] [algebra R A] (f : M →ₗ[R] A) : tensor_algebra R M →ₐ[R] A :=
-ring_quot.lift_alg_hom R (free_algebra.lift R M ⇑f) (λ x y h, by induction h; simp [algebra.smul_def])
+ring_quot.lift_alg_hom R (free_algebra.lift R ⇑f) (λ x y h, by induction h; simp [algebra.smul_def])
 
-variables {R M}
+variables {R}
 
 @[simp]
 theorem ι_comp_lift {A : Type*} [semiring A] [algebra R A] (f : M →ₗ[R] A) :
-  (lift R M f).to_linear_map.comp (ι R M) = f := by { ext, simp [lift, ι], }
+  (lift R f).to_linear_map.comp (ι R) = f := by { ext, simp [lift, ι], }
 
 @[simp]
 theorem lift_ι_apply {A : Type*} [semiring A] [algebra R A] (f : M →ₗ[R] A) (x) :
-  lift R M f (ι R M x) = f x := by { dsimp [lift, ι], refl, }
+  lift R f (ι R x) = f x := by { dsimp [lift, ι], refl, }
 
 @[simp]
 theorem lift_unique {A : Type*} [semiring A] [algebra R A] (f : M →ₗ[R] A)
-  (g : tensor_algebra R M →ₐ[R] A) : g.to_linear_map.comp (ι R M) = f ↔ g = lift R M f :=
+  (g : tensor_algebra R M →ₐ[R] A) : g.to_linear_map.comp (ι R) = f ↔ g = lift R f :=
 begin
   refine ⟨λ hyp, _, λ hyp, by rw [hyp, ι_comp_lift]⟩,
   ext,
@@ -103,14 +104,14 @@ attribute [irreducible] tensor_algebra ι lift
 
 @[simp]
 theorem lift_comp_ι {A : Type*} [semiring A] [algebra R A] (g : tensor_algebra R M →ₐ[R] A) :
-  lift R M (g.to_linear_map.comp (ι R M)) = g := by {symmetry, rw ←lift_unique}
+  lift R (g.to_linear_map.comp (ι R)) = g := by {symmetry, rw ←lift_unique}
 
 @[ext]
 theorem hom_ext {A : Type*} [semiring A] [algebra R A] {f g : tensor_algebra R M →ₐ[R] A}
-  (w : f.to_linear_map.comp (ι R M) = g.to_linear_map.comp (ι R M)) : f = g :=
+  (w : f.to_linear_map.comp (ι R) = g.to_linear_map.comp (ι R)) : f = g :=
 begin
-  let h := g.to_linear_map.comp (ι R M),
-  have : g = lift R M h, by rw ←lift_unique,
+  let h := g.to_linear_map.comp (ι R),
+  have : g = lift R h, by rw ←lift_unique,
   rw [this, ←lift_unique, w],
 end