English
An unramified free algebra is finitely generated. This is the core Iversen I.2.8 result.
Русский
Неразветвленная свободная алгебра конечного типа является конечной породой. Это результат Иверсена I.2.8.
LaTeX
$$$\\text{If } S \\text{ is free as an } R\\text{-module, then } S \\text{ is finite over } R$$$
Lean4
/-- Proposition I.2.3 of [iversen]
If `S` is an unramified `R`-algebra, and `M` is a `S`-module, then the map
`S ⊗[R] M →ₗ[S] M` taking `(b, m) ↦ b • m` admits a `S`-linear section. -/
noncomputable def sec : M →ₗ[S] S ⊗[R] M
where
__ :=
((TensorProduct.AlgebraTensorModule.mapBilinear R S S S S S M LinearMap.id).flip (elem R S)).comp
(lsmul R R M).toLinearMap.flip
map_smul' r
m :=
by
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.coe_comp, Function.comp_apply,
LinearMap.flip_apply, TensorProduct.AlgebraTensorModule.mapBilinear_apply, RingHom.id_apply]
trans
(TensorProduct.AlgebraTensorModule.map (LinearMap.id (R := S) (M := S))
((LinearMap.flip (AlgHom.toLinearMap (lsmul R R M))) m))
((1 ⊗ₜ r) * elem R S)
· induction elem R S using TensorProduct.induction_on
· simp
· simp [smul_comm r]
· simp only [map_add, mul_add, *]
· have := one_tmul_sub_tmul_one_mul_elem (R := R) r
rw [sub_mul, sub_eq_zero] at this
rw [this]
induction elem R S using TensorProduct.induction_on
· simp
· simp [TensorProduct.smul_tmul']
· simp only [map_add, smul_add, mul_add, *]
