[Merged by Bors] - feat(RingTheory/Kaehler): The exact sequence I/I² → B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → 0

[erdOne]

---

[github-actions]

PR summary 8ee44bc6f2

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Kaehler.Basic	1150	1151	+1 (+0.09%)

---

Declarations diff

+ KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange
+ KaehlerDifferential.kerCotangentToTensor
+ KaehlerDifferential.kerCotangentToTensor_toCotangent
+ KaehlerDifferential.kerToTensor
+ KaehlerDifferential.ker_map_of_surjective
+ KaehlerDifferential.mapBaseChange_surjective
+ KaehlerDifferential.range_kerCotangentToTensor
+ KaehlerDifferential.subsingleton_of_surjective

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[riccardobrasca]

Can you avoid tactic mode here?

[erdOne]

The hole is a Prop, so I think it's fine?

[riccardobrasca]

I mean something like

noncomputable
def KaehlerDifferential.kerCotangentToTensor :
    (RingHom.ker (algebraMap A B)).Cotangent →ₗ[A] B ⊗[A] Ω[A⁄R] :=
  Submodule.liftQ _ (kerToTensor R A B) (iSup_le_iff.mpr (by
    simp only [Submodule.map_le_iff_le_comap, Subtype.forall]
    rintro x hx y -
    simp only [Submodule.mem_comap, LinearMap.lsmul_apply, LinearMap.mem_ker, map_smul,
      kerToTensor_apply, TensorProduct.smul_tmul', ← algebraMap_eq_smul_one,
      (RingHom.mem_ker _).mp hx, TensorProduct.zero_tmul]))

Or to prove the thing in a separate lemma (tbh I didn't look at what it is, so I am not sure this is reasonable).

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[erdOne]

Thanks!
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style