refactor(algebra/free_algebra): Make lift an equiv (#4908)

This can probably lead to some API cleanup down the line

src/algebra/category/Algebra/basic.lean

@@ -82,17 +82,12 @@ def free : Type* ⥤ Algebra R :=
   map := λ S T f, free_algebra.lift _ $ (free_algebra.ι _) ∘ f }
 
 /-- The free/forget ajunction for `R`-algebras. -/
-@[simps]
 def adj : free R ⊣ forget (Algebra R) :=
-{ hom_equiv := λ X A,
-  { to_fun := λ f, f ∘ (free_algebra.ι _),
-    inv_fun := λ f, free_algebra.lift _ f,
-    left_inv := by tidy,
-    right_inv := by tidy },
-  unit := { app := λ S, free_algebra.ι _ },
-  counit :=
-  { app := λ S, free_algebra.lift _ $ id,
-    naturality' := by {intros, ext, simp} } } -- tidy times out :(
+adjunction.mk_of_hom_equiv
+{ hom_equiv := λ X A, (free_algebra.lift _).symm,
+  -- Relying on `obviously` to fill out these proofs is very slow :(
+  hom_equiv_naturality_left_symm' := by {intros, ext, simp},
+  hom_equiv_naturality_right' := by {intros, ext, simp} }
 
 end Algebra
 

src/algebra/free_algebra.lean

@@ -186,11 +186,8 @@ def ι : X → free_algebra R X := λ m, quot.mk _ m
 
 variables {A : Type*} [semiring A] [algebra R A]
 
-/--
-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 (f : X → A) : free_algebra R X →ₐ[R] A :=
+/-- Internal definition used to define `lift` -/
+private def lift_aux (f : X → A) : (free_algebra R X →ₐ[R] A) :=
 { to_fun := λ a, quot.lift_on a (lift_fun _ _ f) $ λ a b h,
   begin
     induction h,
@@ -230,6 +227,36 @@ def lift (f : X → A) : free_algebra R X →ₐ[R] A :=
   map_add' := by { rintros ⟨⟩ ⟨⟩, refl },
   commutes' := by tauto }
 
+/--
+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 : (X → A) ≃ (free_algebra R X →ₐ[R] A) :=
+{ to_fun := lift_aux R,
+  inv_fun := λ F, F ∘ (ι R),
+  left_inv := λ f, by {ext, refl},
+  right_inv := λ F, by {
+    ext x,
+    rcases x,
+    induction x,
+    case pre.of : {
+      change ((F : free_algebra R X → A) ∘ (ι R)) _ = _,
+      refl },
+    case pre.of_scalar : {
+      change algebra_map _ _ x = F (algebra_map _ _ x),
+      rw alg_hom.commutes F x, },
+    case pre.add : a b ha hb {
+      change lift_aux R (F ∘ ι R) (quot.mk _ _ + quot.mk _ _) = F (quot.mk _ _ + quot.mk _ _),
+      rw [alg_hom.map_add, alg_hom.map_add, ha, hb], },
+    case pre.mul : a b ha hb {
+      change lift_aux R (F ∘ ι R) (quot.mk _ _ * quot.mk _ _) = F (quot.mk _ _ * quot.mk _ _),
+      rw [alg_hom.map_mul, alg_hom.map_mul, ha, hb], }, }, }
+
+@[simp] lemma lift_aux_eq (f : X → A) : lift_aux R f = lift R f := rfl
+
+@[simp]
+lemma lift_symm_apply (F : free_algebra R X →ₐ[R] A) : (lift R).symm F = F ∘ (ι R) := rfl
+
 variables {R X}
 
 @[simp]
@@ -243,22 +270,7 @@ theorem lift_ι_apply (f : X → A) (x) :
 @[simp]
 theorem lift_unique (f : X → A) (g : free_algebra R X →ₐ[R] A) :
   (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)) _ = _,
-    rw hyp,
-    refl },
-  { exact alg_hom.commutes g x },
-  { change g (quot.mk _ _ + quot.mk _ _) = _,
-    simp only [alg_hom.map_add, *],
-    refl },
-  { change g (quot.mk _ _ * quot.mk _ _) = _,
-    simp only [alg_hom.map_mul, *],
-    refl },
-end
+(lift R).symm_apply_eq
 
 /-!
 At this stage we set the basic definitions as `@[irreducible]`, so from this point onwards one should only use the universal properties of the free algebra, and consider the actual implementation as a quotient of an inductive type as completely hidden.
@@ -272,14 +284,15 @@ attribute [irreducible] ι lift
 
 @[simp]
 theorem lift_comp_ι (g : free_algebra R X →ₐ[R] A) :
-  lift R ((g : free_algebra R X → A) ∘ (ι R)) = g := by {symmetry, rw ←lift_unique}
+  lift R ((g : free_algebra R X → A) ∘ (ι R)) = g :=
+by { rw ←lift_symm_apply, exact (lift R).apply_symm_apply g }
 
 @[ext]
 theorem hom_ext {f g : free_algebra R X →ₐ[R] A}
   (w : ((f : free_algebra R X → A) ∘ (ι R)) = ((g : free_algebra R X → A) ∘ (ι R))) : f = g :=
 begin
-  have : g = lift R ((g : free_algebra R X → A) ∘ (ι R)), by rw ←lift_unique,
-  rw [this, ←lift_unique, w],
+  rw [←lift_symm_apply, ←lift_symm_apply] at w,
+  exact (lift R).symm.injective w,
 end
 
 /--

src/algebra/lie/universal_enveloping.lean

@@ -77,43 +77,43 @@ 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 (f : L →ₗ[R] A))
-begin
-  intros a b h, induction h with x y,
-  simp [lie_ring.of_associative_ring_bracket],
-end
+def lift : (L →ₗ⁅R⁆ A) ≃ (universal_enveloping_algebra R L →ₐ[R] A) :=
+{ to_fun := λ f,
+    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⟩,
+  inv_fun := λ F, (lie_algebra.of_associative_algebra_hom F).comp (ι R),
+  left_inv := λ f, by { ext, simp [ι, mk_alg_hom], },
+  right_inv := λ F, by { ext, simp [ι, mk_alg_hom], } }
+
+@[simp] lemma lift_symm_apply (F : universal_enveloping_algebra R L →ₐ[R] A) :
+  (lift R).symm F = (lie_algebra.of_associative_algebra_hom F).comp (ι R) :=
+rfl
+
+@[simp] lemma ι_comp_lift : (lift R f) ∘ (ι R) = f :=
+funext $ lie_algebra.morphism.ext_iff.mp $ (lift R).symm_apply_apply f
 
 @[simp] lemma lift_ι_apply (x : L) : lift R f (ι R x) = f x :=
-begin
-  have : ι R x = ring_quot.mk_alg_hom R (rel R L) (ιₜ x), by refl,
-  simp [this, lift],
-end
-
-lemma ι_comp_lift : (lift R f) ∘ (ι R) = f :=
-by { ext, simp, }
+by rw [←function.comp_apply (lift R f) (ι R) x, ι_comp_lift]
 
 lemma lift_unique (g : universal_enveloping_algebra R L →ₐ[R] A) :
   g ∘ (ι R) = f ↔ g = lift R f :=
 begin
-  split; intros h,
-  { apply ring_quot.lift_alg_hom_unique,
-    rw ← tensor_algebra.lift_unique,
-    ext x,
-    change _ = f x, rw ← congr h rfl,
-    refl, },
-  { subst h, apply ι_comp_lift, },
+  refine iff.trans _ (lift R).symm_apply_eq,
+  split; {intro h, ext, simp [←h] },
 end
 
 @[ext] lemma hom_ext {g₁ g₂ : universal_enveloping_algebra R L →ₐ[R] A}
   (h : g₁ ∘ (ι R) = g₂ ∘ (ι R)) : g₁ = g₂ :=
 begin
-  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 f₁, { rw ← lift_unique, refl, },
-  have h₂ : g₂ = lift R f₂, { rw ← lift_unique, refl, },
-  rw [h₁, h₂, h'],
+  apply (lift R).symm.injective,
+  rw [lift_symm_apply, lift_symm_apply],
+  ext x,
+  have := congr h (rfl : x = x),
+  rw function.comp_apply at this,
+  simp [this],
 end
 
 end universal_enveloping_algebra

src/algebra/ring_quot.lean

@@ -129,36 +129,41 @@ variables  {T : Type u₄} [semiring T]
 
 /--
 Any ring homomorphism `f : R →+* T` which respects a relation `r : R → R → Prop`
-factors through a morphism `ring_quot r →+* T`.
+factors uniquely through a morphism `ring_quot r →+* T`.
 -/
-def lift (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y) :
-  ring_quot r →+* T :=
-{ to_fun := quot.lift f
-  begin
-    rintros _ _ r,
-    induction r,
-    case of : _ _ r { exact w r, },
-    case add_left : _ _ _ _ r' { simp [r'], },
-    case mul_left : _ _ _ _ r' { simp [r'], },
-    case mul_right : _ _ _ _ r' { simp [r'], },
-  end,
-  map_zero' := f.map_zero,
-  map_add' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_add x y, },
-  map_one' := f.map_one,
-  map_mul' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_mul x y, }, }
+def lift {r : R → R → Prop} :
+  {f : R →+* T // ∀ ⦃x y⦄, r x y → f x = f y} ≃ (ring_quot r →+* T) :=
+{ to_fun := λ f', let f := (f' : R →+* T) in
+  { to_fun := quot.lift f
+    begin
+      rintros _ _ r,
+      induction r,
+      case of : _ _ r { exact f'.prop r, },
+      case add_left : _ _ _ _ r' { simp [r'], },
+      case mul_left : _ _ _ _ r' { simp [r'], },
+      case mul_right : _ _ _ _ r' { simp [r'], },
+    end,
+    map_zero' := f.map_zero,
+    map_add' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_add x y, },
+    map_one' := f.map_one,
+    map_mul' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_mul x y, }, },
+  inv_fun := λ F, ⟨F.comp (mk_ring_hom r), λ x y h, by { dsimp, rw mk_ring_hom_rel h, }⟩,
+  left_inv := λ f, by { ext, simp, refl },
+  right_inv := λ F, by { ext, simp, refl } }
 
 @[simp]
 lemma lift_mk_ring_hom_apply (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y) (x) :
-  (lift f w) (mk_ring_hom r x) = f x :=
+  lift ⟨f, w⟩ (mk_ring_hom r x) = f x :=
 rfl
 
+-- note this is essentially `lift.symm_apply_eq.mp h`
 lemma lift_unique (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y)
-  (g : ring_quot r →+* T) (h : g.comp (mk_ring_hom r) = f) : g = lift f w :=
+  (g : ring_quot r →+* T) (h : g.comp (mk_ring_hom r) = f) : g = lift ⟨f, w⟩ :=
 by { ext, simp [h], }
 
 lemma eq_lift_comp_mk_ring_hom {r : R → R → Prop} (f : ring_quot r →+* T) :
-  f = lift (f.comp (mk_ring_hom r)) (λ x y h, by { dsimp, rw mk_ring_hom_rel h, }) :=
-by { ext, simp, }
+  f = lift ⟨f.comp (mk_ring_hom r), λ x y h, by { dsimp, rw mk_ring_hom_rel h, }⟩ :=
+(lift.apply_symm_apply f).symm
 
 section comm_ring
 /-!
@@ -172,8 +177,8 @@ variables {B : Type u₁} [comm_ring B]
 def ring_quot_to_ideal_quotient (r : B → B → Prop) :
   ring_quot r →+* (ideal.of_rel r).quotient :=
 lift
-  (ideal.quotient.mk (ideal.of_rel r))
-  (λ x y h, quot.sound (submodule.mem_Inf.mpr (λ p w, w ⟨x, y, h, rfl⟩)))
+  ⟨ideal.quotient.mk (ideal.of_rel r),
+   λ x y h, quot.sound (submodule.mem_Inf.mpr (λ p w, w ⟨x, y, h, rfl⟩))⟩
 
 @[simp] lemma ring_quot_to_ideal_quotient_apply (r : B → B → Prop) (x : B) :
   ring_quot_to_ideal_quotient r (mk_ring_hom r x) = ideal.quotient.mk _ x := rfl
@@ -240,43 +245,48 @@ end
 
 /--
 Any `S`-algebra homomorphism `f : A →ₐ[S] B` which respects a relation `s : A → A → Prop`
-factors through a morphism `ring_quot s →ₐ[S]  B`.
+factors uniquely through a morphism `ring_quot s →ₐ[S]  B`.
 -/
-def lift_alg_hom (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y⦄, s x y → f x = f y) :
-  ring_quot s →ₐ[S] B :=
-{ to_fun := quot.lift f
-  begin
-    rintros _ _ r,
-    induction r,
-    case of : _ _ r { exact w r, },
-    case add_left : _ _ _ _ r' { simp [r'], },
-    case mul_left : _ _ _ _ r' { simp [r'], },
-    case mul_right : _ _ _ _ r' { simp [r'], },
-  end,
-  map_zero' := f.map_zero,
-  map_add' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_add x y, },
-  map_one' := f.map_one,
-  map_mul' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_mul x y, },
-  commutes' :=
-  begin
-    rintros x,
-    conv_rhs { rw [algebra.algebra_map_eq_smul_one, ←f.map_one, ←f.map_smul], },
-    rw algebra.algebra_map_eq_smul_one,
-    exact quot.lift_beta f @w (x • 1),
-  end, }
+def lift_alg_hom {s : A → A → Prop} :
+  { f : A →ₐ[S] B // ∀ ⦃x y⦄, s x y → f x = f y} ≃ (ring_quot s →ₐ[S] B) :=
+{ to_fun := λ f', let f := (f' : A →ₐ[S] B) in
+  { to_fun := quot.lift f
+    begin
+      rintros _ _ r,
+      induction r,
+      case of : _ _ r { exact f'.prop r, },
+      case add_left : _ _ _ _ r' { simp [r'], },
+      case mul_left : _ _ _ _ r' { simp [r'], },
+      case mul_right : _ _ _ _ r' { simp [r'], },
+    end,
+    map_zero' := f.map_zero,
+    map_add' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_add x y, },
+    map_one' := f.map_one,
+    map_mul' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_mul x y, },
+    commutes' :=
+    begin
+      rintros x,
+      conv_rhs { rw [algebra.algebra_map_eq_smul_one, ←f.map_one, ←f.map_smul], },
+      rw algebra.algebra_map_eq_smul_one,
+      exact quot.lift_beta f f'.prop (x • 1),
+    end, },
+  inv_fun := λ F, ⟨F.comp (mk_alg_hom S s), λ _ _ h, by { dsimp, erw mk_alg_hom_rel S h }⟩,
+  left_inv := λ f, by { ext, simp, refl },
+  right_inv := λ F, by { ext, simp, refl } }
 
 @[simp]
 lemma lift_alg_hom_mk_alg_hom_apply (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y⦄, s x y → f x = f y) (x) :
-  (lift_alg_hom S f w) ((mk_alg_hom S s) x) = f x :=
+  (lift_alg_hom S ⟨f, w⟩) ((mk_alg_hom S s) x) = f x :=
 rfl
 
+-- note this is essentially `(lift_alg_hom S).symm_apply_eq.mp h`
 lemma lift_alg_hom_unique (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y⦄, s x y → f x = f y)
-  (g : ring_quot s →ₐ[S] B) (h : g.comp (mk_alg_hom S s) = f) : g = lift_alg_hom S f w :=
+  (g : ring_quot s →ₐ[S] B) (h : g.comp (mk_alg_hom S s) = f) : g = lift_alg_hom S ⟨f, w⟩ :=
 by { ext, simp [h], }
 
 lemma eq_lift_alg_hom_comp_mk_alg_hom {s : A → A → Prop} (f : ring_quot s →ₐ[S] B) :
-  f = lift_alg_hom S (f.comp (mk_alg_hom S s)) (λ x y h, by { dsimp, erw mk_alg_hom_rel S h, }) :=
-by { ext, simp, }
+  f = lift_alg_hom S ⟨f.comp (mk_alg_hom S s), λ x y h, by { dsimp, erw mk_alg_hom_rel S h, }⟩ :=
+((lift_alg_hom S).apply_symm_apply f).symm
 
 end algebra