English
If there is a ring equivalence e1: R ≃+* S and a compatible linear equivalence e2: M ≃ₛₗ N, then projectivity is preserved, i.e., if M is projective over R, then N is projective over S.
Русский
Если существует эквивалентность колец e1: R ≃+* S и совместимая линейная эквивалентность e2: M ≃ₛₗ N, то проективность сохраняется: если M проективен над R, то N проективен над S.
LaTeX
$$$$ \\text{If } e_1,e_2 \\text{ as above and } M \\text{ is projective over } R, \\text{ then } N \\text{ is projective over } S. $$$$
Lean4
instance tensorProduct [hM : Module.Projective R M] [hN : Module.Projective R₀ N] : Module.Projective R (M ⊗[R₀] N) :=
by
obtain ⟨sM, hsM⟩ := hM
obtain ⟨sN, hsN⟩ := hN
have : Module.Projective R (M ⊗[R₀] (N →₀ R₀)) :=
by
fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
· exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))
· exact (AlgebraTensorModule.map (Finsupp.linearCombination R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))
· ext; simp [hsM _]
fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))
· exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) sN)
· exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) (linearCombination R₀ id))
· ext; simp [hsN _]
