feat(RingTheory/Extension): fromH1Cotangent

[BryceT233]

This PR is a continuation of #39520. For an extension P : Extension R S, we introduce fromH1Cotangent, a linear map from H1Cotangent R S to P.H1Cotangent induced by the default extension homomorphism. We show that the following diagram commutes:

Finally, by combining this commutativity lemma with the exactness of Jacobi-Zariski sequence, we prove that fromH1Cotangent is surjective.

---

• depends on: feat(RingTheory/Extension): cotangentEquivH1Cotangent #39520

[github-actions]

PR summary c6ccf096e3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Cotangent.map_comp_apply
+ coe_cotangentEquivH1Cotangent_comp_fromH1Cotangent
+ cotangentEquivH1Cotangent
+ fromH1Cotangent
+ fromH1Cotangent_surjective
+ h1Cotangentδ_comp_coe_cotangentEquivH1Cotangent

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(RingTheory/Extension): cotangentEquivH1Cotangent #39520
  By Dependent Issues (🤖). Happy coding!