tensorH1Cotangent — Mathlib

English

Coherence of tensorCotangentInvFun with respect to equalities between morphisms follows from a functorial pushout/pullback style reasoning for cotangent spaces in the étale setting; congruence ensures independence from the chosen representatives of the same map.

Русский

Согласованность tensorCotangentInvFun по отношению к равенствам морфизмов следует из функториального рассуждения о пушбах и пулбакх котангенентальных пространств в этиальном контексте: конгруэнтность обеспечивает независимость от выбранных репрезентантов одного и того же отображения.

LaTeX

$$$\\text{tensorCotangentInvFun}$ congruent under equality of morphisms$$

Lean4

/-- If `J ≃ Q ⊗ₚ I`, `S → T` is flat and `P → Q` is formally étale, then `T ⊗ H¹(L_P) ≃ H¹(L_Q)`. -/
noncomputable def tensorH1Cotangent [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
    [Module.Flat S T] (H₁ : f.toRingHom.FormallyEtale)
    (H₂ : Function.Bijective ((f.mapKer halg).liftBaseChange Q.Ring)) : T ⊗[S] P.H1Cotangent ≃ₗ[T] Q.H1Cotangent :=
  by
  refine .ofBijective ((H1Cotangent.map f).liftBaseChange T) ?_
  constructor
  · rw [injective_iff_map_eq_zero]
    intro x hx
    apply Module.Flat.lTensor_preserves_injective_linearMap _ h1Cotangentι_injective
    apply (Extension.tensorCotangent f halg H₂).injective
    simp only [map_zero]
    rw [← h1Cotangentι.map_zero, ← hx]
    change ((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange T) x = (h1Cotangentι ∘ₗ _) x
    congr 1
    ext x
    simp
  · intro x
    have : Function.Exact (h1Cotangentι.baseChange T) (P.cotangentComplex.baseChange T) :=
      Module.Flat.lTensor_exact T (LinearMap.exact_subtype_ker_map _)
    obtain ⟨a, ha⟩ :=
      (this ((Extension.tensorCotangent f halg H₂).symm x.1)).mp
        (by
          apply (Extension.tensorCotangentSpace f H₁).injective
          rw [LinearEquiv.map_zero, ← x.2]
          have :
            (CotangentSpace.map f).liftBaseChange T ∘ₗ P.cotangentComplex.baseChange T =
              Q.cotangentComplex ∘ₗ (Cotangent.map f).liftBaseChange T :=
            by
            ext x; obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x; dsimp
            simp only [CotangentSpace.map_tmul, map_one, Hom.toAlgHom_apply, one_smul, cotangentComplex_mk]
          exact
            (DFunLike.congr_fun this _).trans
              (DFunLike.congr_arg Q.cotangentComplex ((tensorCotangent f halg H₂).apply_symm_apply x.1)))
    refine ⟨a, Subtype.ext (.trans ?_ ((LinearEquiv.eq_symm_apply _).mp ha))⟩
    change
      (h1Cotangentι ∘ₗ (H1Cotangent.map f).liftBaseChange T) _ =
        ((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange T) _
    congr 1
    ext; dsimp

Похожие утверждения