new proof found by Aristotle

LocallyFreeOfInvertible.lean

import Mathlib

variable (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M]
variable [Module.Invertible R M]

/-!
# Invertible modules are Zariski-locally free

We show that an invertible module over a commutative semiring is Zariski-locally free of rank 1,
and that over a local semiring it is free.

The key idea is that bijectivity of `contractLeft R M` gives elements `fᵢ ∈ M∨`, `mᵢ ∈ M` with
`∑ fᵢ(mᵢ) = 1`. Over a local ring one of these evaluations is a unit, making the corresponding
dual functional surjective; surjectivity plus invertibility gives bijectivity via
`Module.Invertible.bijective_of_surjective`, hence `M ≃ₗ[R] R`. For the Zariski-local
statement we localise at each `fᵢ(mᵢ)`, which becomes a unit in the localisation.

## Main results

* `Module.Invertible.free`: An invertible module over a local semiring is free.
* `Module.Invertible.locally_free`: An invertible module is Zariski-locally free.
-/

private theorem exists_finset_sum_eq_one :
    ∃ S : Finset (Module.Dual R M × M), ∑ i ∈ S, i.1 i.2 = 1 := by
  obtain ⟨S, hS⟩ := TensorProduct.exists_finset ((Module.Invertible.linearEquiv R M).symm 1)
  refine ⟨S, ?_⟩
  have : contractLeft R M (∑ i ∈ S, i.1 ⊗ₜ[R] i.2) = 1 := by
    rw [← hS]; exact (Module.Invertible.linearEquiv R M).apply_symm_apply 1
  rwa [map_sum] at this

/-- An invertible module over a local semiring is free.

The evaluations `fᵢ(mᵢ)` obtained from the inverse of `contractLeft` sum to `1`;
over a local ring one must be a unit, whence the corresponding dual functional is surjective
and therefore bijective (by `Module.Invertible.bijective_of_surjective`), giving `M ≃ₗ[R] R`. -/
theorem Module.Invertible.free [IsLocalRing R] : Module.Free R M := by
  obtain ⟨S, hS⟩ := exists_finset_sum_eq_one R M
  by_contra hfree
  have hmem : ∀ i ∈ S, i.1 i.2 ∈ IsLocalRing.maximalIdeal R := by
    intro i hi
    rw [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff]
    intro hu
    exact hfree (free_iff_linearEquiv.mpr
      ⟨LinearEquiv.ofBijective i.1
        (bijective_of_surjective fun r =>
          ⟨(r * ↑hu.unit⁻¹) • i.2, by
            simp only [map_smul, smul_eq_mul, mul_assoc, IsUnit.val_inv_mul, mul_one]⟩)⟩)
  exact (IsLocalRing.maximalIdeal.isMaximal R).ne_top
    ((Ideal.eq_top_iff_one _).mpr (hS ▸ Ideal.sum_mem _ hmem))

/-- An invertible module over a commutative semiring is Zariski-locally free of rank 1.

More precisely, there is a finite set of elements of `R` that generate the unit ideal,
and localising `M` at any one of them yields a free module. -/
theorem Module.Invertible.locally_free :
    ∃ s : Set R, Ideal.span s = ⊤ ∧ ∀ r ∈ s,
      Module.Free (Localization.Away r) (LocalizedModule.Away r M) := by
  classical
  obtain ⟨S, hS⟩ := exists_finset_sum_eq_one R M
  refine ⟨Finset.image (fun i => i.1 i.2) S, ?_, ?_⟩
  -- The evaluations generate the unit ideal
  · rw [Ideal.eq_top_iff_one, ← hS]
    exact Ideal.sum_mem _ fun i hi =>
      Ideal.subset_span (Finset.mem_coe.mpr (Finset.mem_image.mpr ⟨i, hi, rfl⟩))
  -- After localising at any evaluation, the module becomes free
  · intro r hr
    rw [Finset.mem_coe, Finset.mem_image] at hr
    obtain ⟨⟨f, m⟩, _, rfl⟩ := hr
    -- f(m) becomes a unit in Localization.Away (f m)
    have hu : IsUnit (algebraMap R (Localization.Away (f m)) (f m)) :=
      IsLocalization.Away.algebraMap_isUnit (f m)
    -- Extend f to a Localization.Away (f m)-linear dual on the localised module
    set f' : Module.Dual (Localization.Away (f m)) (LocalizedModule.Away (f m) M) :=
      LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (f m)) _
        (IsLocalizedModule.map (Submonoid.powers (f m)) (LocalizedModule.mkLinearMap _ M)
          (Algebra.linearMap R (Localization.Away (f m))) f)
    -- f' evaluated at the image of m gives algebraMap (f m), a unit
    have hval : f' (LocalizedModule.mkLinearMap _ M m) = algebraMap R _ (f m) := by
      change (IsLocalizedModule.map _ (LocalizedModule.mkLinearMap _ M) _ f) _ = _
      exact IsLocalizedModule.map_apply _ _ _ f m
    -- f' is surjective: for any a, f'(a · (f m)⁻¹ · m) = a
    have hsurj : Function.Surjective f' := fun a =>
      ⟨(a * ↑hu.unit⁻¹) • LocalizedModule.mkLinearMap _ M m, by
        rw [map_smul, smul_eq_mul, hval, mul_assoc, IsUnit.val_inv_mul, mul_one]⟩
    exact free_iff_linearEquiv.mpr
      ⟨LinearEquiv.ofBijective f' (bijective_of_surjective hsurj)⟩