feat(ring_theory/algebra_tower): alg_hom_equiv_sigma (#5345)

Proves that algebra homomorphisms from the top of an is_scalar_tower are the same as a pair of algebra homomorphisms.

This is useful for counting algebra homomorphisms.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/ring_theory/algebra_tower.lean

@@ -458,3 +458,36 @@ by exactI fg_of_injective (is_scalar_tower.to_alg_hom B₀ B C).to_linear_map
   (linear_map.ker_eq_bot.2 hBCi)
 
 end artin_tate
+
+section alg_hom_tower
+
+variables {A} {C D : Type*} [comm_semiring A] [comm_semiring C] [comm_semiring D]
+  [algebra A C] [algebra A D]
+
+variables (f : C →ₐ[A] D) (B) [comm_semiring B] [algebra A B] [algebra B C] [is_scalar_tower A B C]
+
+/-- Restrict the domain of an `alg_hom`. -/
+def alg_hom.restrict_domain : B →ₐ[A] D := f.comp (is_scalar_tower.to_alg_hom A B C)
+
+/-- Extend the scalars of an `alg_hom`. -/
+def alg_hom.extend_scalars : @alg_hom B C D _ _ _ _ (f.restrict_domain B).to_ring_hom.to_algebra :=
+{ commutes' := λ _, rfl .. f }
+
+variables {B}
+
+/-- `alg_hom`s from the top of a tower are equivalent to a pair of `alg_hom`s. -/
+def alg_hom_equiv_sigma :
+  (C →ₐ[A] D) ≃ Σ (f : B →ₐ[A] D), @alg_hom B C D _ _ _ _ f.to_ring_hom.to_algebra :=
+{ to_fun := λ f, ⟨f.restrict_domain B, f.extend_scalars B⟩,
+  inv_fun := λ fg, @is_scalar_tower.restrict_base A _ _ _ _ _ _ _ _ _
+    fg.1.to_ring_hom.to_algebra _ _ _ _ fg.2,
+  left_inv := λ f, by { dsimp only, ext, refl },
+  right_inv :=
+  begin
+    rintros ⟨⟨f, _, _, _, _, _⟩, g, _, _, _, _, hg⟩,
+    have : f = λ x, g (algebra_map B C x) := by { ext, exact (hg x).symm },
+    subst this,
+    refl,
+  end }
+
+end alg_hom_tower