RegularLocalTrace.lean

theorem trace_add_of_exact
    {K : Type v} [Field K]
    {A : Type w₁} [AddCommGroup A] [Module K A] [Module.Finite K A]
    {F : Type w₂} [AddCommGroup F] [Module K F] [Module.Finite K F]
    {M : Type w₃} [AddCommGroup M] [Module K M] [Module.Finite K M]
    (i : A →ₗ[K] F) (p : F →ₗ[K] M)
    (hi : Function.Injective i) (hp : Function.Surjective p)
    (hex : Function.Exact i p)
    (a : Module.End K A) (b : Module.End K F) (c : Module.End K M)
    (hbi : b.comp i = i.comp a) (hpb : p.comp b = c.comp p) :
    LinearMap.trace K F b = LinearMap.trace K A a + LinearMap.trace K M c

theorem trace_baseChange_mem_range_of_hasFFR
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    (K : Type v) [Field K] [Algebra R K] [Module.Flat R K]
    (n : ℕ) : ∀ (M : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M],
      HasFFR R n M → ∀ φ : Module.End R M,
        ∃ r : R, algebraMap R K r = LinearMap.trace K (K ⊗[R] M) (φ.baseChange K)

theorem trace_baseChange_mem_range_of_isRegularLocalRing
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (K : Type v) [Field K] [Algebra R K] [Module.Flat R K]
    (M : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (φ : Module.End R M) :
    ∃ r : R, algebraMap R K r = LinearMap.trace K (K ⊗[R] M) (φ.baseChange K)

theorem isIntegrallyClosed_of_isRegularLocalRing
    (R : Type u) [CommRing R] [IsRegularLocalRing R] : IsIntegrallyClosed R