Lifting semilinear maps out of a projective module

Let σ : R →+* S be a ring homomorphism, P a projective R-module and F : M → N a surjective S-linear map. Then every σ-semilinear map P → N lifts through F to a σ-semilinear map P → M. This is Mathlib's lifting property Module.projective_lifting_property applied to M and N with scalars restricted along σ, since a σ-semilinear map out of P is an R-linear map into the restricted module.

It is the form of the lifting property used to show that extension of scalars along a ring homomorphism of possibly noncommutative rings preserves projectivity: an S-linear map out of S ⊗_R P is the same as a σ-semilinear map out of P.

Main results

• Module.projective_lifting_property_semilinear: semilinear maps out of a projective module lift along surjective linear maps.
• Module.exists_surjective_projective_ker_of_semilinearEquiv: a presentation with projective kernel transports along a semilinear equivalence.

theorem Module.projective_lifting_property_semilinear {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {σ : R →+* S} {P : Type u_3} [AddCommMonoid P] [Module R P] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [Module S M] [AddCommMonoid N] [Module S N] [Projective R P] (F : M →ₗ[S] N) (hF : Function.Surjective ⇑F) (g : P →ₛₗ[σ] N) : ∃ (h : P →ₛₗ[σ] M), F ∘ₛₗ h = g

The lifting property of a projective module, for semilinear maps. If P is a projective R-module and F : M →ₗ[S] N is surjective, then every σ-semilinear map g : P → N factors as F ∘ h for a σ-semilinear map h : P → M.

theorem Module.exists_surjective_projective_ker_of_semilinearEquiv {R : Type u_6} {R' : Type u_7} [Semiring R] [Semiring R'] {M : Type u_8} {M' : Type u_9} [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R' M'] (Φ : R ≃+* R') [RingHomInvPair ↑Φ ↑Φ.symm] [RingHomInvPair ↑Φ.symm ↑Φ] (e : M ≃ₛₗ[↑Φ] M') {ι : Type u_10} (f' : (ι → R') →ₗ[R'] M') (hf' : Function.Surjective ⇑f') (hker : Projective R' ↥f'.ker) : ∃ (f : (ι → R) →ₗ[R] M), Function.Surjective ⇑f ∧ Projective R ↥f.ker

A presentation with projective kernel transports along a semilinear equivalence. Let Φ : R ≃+* R' be a ring isomorphism and e : M ≃ₛₗ[Φ] M' a Φ-semilinear equivalence. If M' is a quotient (ι → R') → M' by a projective kernel, then so is M as a quotient of ι → R.