NYLL
Module

FiniteSubalgebraLocalization.lean

Nyll.SchemeTheory.RingTheory.Flat.FiniteSubalgebraLocalization
76 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Finite-subalgebra localization and tensor-kernel generation give finite algebraic models for flat modules.

Imports3
Imported by4

Declarations

def

FreeCover

L39 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.FreeCover
Documentation

The free A-module on the elements of X, implemented as finitely supported functions.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
Lean source · statement
def FreeCover (A : Type u) [CommRing A] (X : Type*) : Type _
instance

(anonymous instance)

L45 ↗
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
namespace FreeCover
variable (A : Type u) [CommRing A] (X : Type*)
Lean source · statement
instance : AddCommGroup (FreeCover A X)
instance

(anonymous instance)

L46 ↗
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
namespace FreeCover
variable (A : Type u) [CommRing A] (X : Type*)
Lean source · statement
instance : Module A (FreeCover A X)
def

equiv

L49 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.FreeCover.equiv
Documentation

The linear equivalence identifying the free cover with its finitely supported functions.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
namespace FreeCover
variable (A : Type u) [CommRing A] (X : Type*)
Lean source · statement
def equiv : FreeCover A X ≃ₗ[A] (X →₀ A)
def

cover

L60 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.cover
Documentation

The canonical surjection from the free module on the elements of N2 to N2.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section KernelGeneration
variable {A : Type u} [CommRing A] {D : Type v} [CommRing D] [Algebra A D]
Lean source · statement
def cover (N₂ : Type*) [AddCommGroup N₂] [Module A N₂] : FreeCover A N₂ →ₗ[A] N₂
theorem

cover_surjective

L63 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.cover_surjective
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section KernelGeneration
variable {A : Type u} [CommRing A] {D : Type v} [CommRing D] [Algebra A D]
Lean source · statement
theorem cover_surjective (N₂ : Type*) [AddCommGroup N₂] [Module A N₂] :
    Function.Surjective (cover (A := A) N₂)
theorem

baseChange_exact

L67 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.baseChange_exact
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section KernelGeneration
variable {A : Type u} [CommRing A] {D : Type v} [CommRing D] [Algebra A D]
Lean source · statement
theorem baseChange_exact {N₁ N₂ N₃ : Type*} [AddCommGroup N₁] [AddCommGroup N₂]
    [AddCommGroup N₃] [Module A N₁] [Module A N₂] [Module A N₃] {f : N₁ →ₗ[A] N₂}
    {g : N₂ →ₗ[A] N₃} (hfg : Function.Exact f g) (hg : Function.Surjective g) :
    Function.Exact (f.baseChange D) (g.baseChange D)
theorem

baseChange_surjective

L74 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.baseChange_surjective
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section KernelGeneration
variable {A : Type u} [CommRing A] {D : Type v} [CommRing D] [Algebra A D]
Lean source · statement
theorem baseChange_surjective {N₁ N₂ : Type*} [AddCommGroup N₁] [AddCommGroup N₂]
    [Module A N₁] [Module A N₂] {f : N₁ →ₗ[A] N₂} (hf : Function.Surjective f) :
    Function.Surjective (f.baseChange D)
def

torKer

L82 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.torKer
Documentation

The kernel of the ideal inclusion after extending scalars to D.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section KernelGeneration
variable {A : Type u} [CommRing A] {D : Type v} [CommRing D] [Algebra A D]
variable (D) in
Lean source · statement
def torKer (J : Ideal A) : Submodule D (D ⊗[A] J)
theorem

mem_span_of_mapRange_baseChange_eq_zero

L85 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.mem_span_of_mapRange_baseChange_eq_zero
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section KernelGeneration
variable {A : Type u} [CommRing A] {D : Type v} [CommRing D] [Algebra A D]
variable (D) in
Lean source · statement
theorem mem_span_of_mapRange_baseChange_eq_zero (J : Ideal A) (ι : Type*)
    (w : D ⊗[A] (ι →₀ J))
    (hw : (Finsupp.mapRange.linearMap (α := ι) (Submodule.subtype J)).baseChange D w = 0) :
    w ∈ Submodule.span D (⋃ i, (Finsupp.lsingle i : J →ₗ[A] (ι →₀ J)).baseChange D ''
      (torKer D J : Set (D ⊗[A] J)))
theorem

exists_generators_of_ker_baseChange

L133 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.exists_generators_of_ker_baseChange
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section KernelGeneration
variable {A : Type u} [CommRing A] {D : Type v} [CommRing D] [Algebra A D]
variable (D) in
Lean source · statement
theorem exists_generators_of_ker_baseChange (J : Ideal A) (S : Submonoid D)
    (hrel : ∀ ⦃Q₁ Q₂ : Type (max u w)⦄ [AddCommGroup Q₁] [AddCommGroup Q₂] [Module A Q₁]
      [Module A Q₂] (g : Q₁ →ₗ[A] Q₂), Function.Injective g →
      Module.IsTorsionBySet A Q₂ J →
      ∀ x : D ⊗[A] Q₁, g.baseChange D x = 0 → ∃ s ∈ S, s • x = 0)
    {N₁ N₂ N : Type w} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N]
    [Module A N₁] [Module A N₂] [Module A N]
    (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N) (hf : Function.Injective f)
    (hfg : Function.Exact f g) (hN : Module.IsTorsionBySet A N J) :
    ∃ γ : N₂ → (J →ₗ[A] N₁), (∀ (n : N₂) (j : J), f (γ n j) = (j : A) • n) ∧
      ∀ x : D ⊗[A] N₁, f.baseChange D x = 0 → ∃ s ∈ S,
        s • x ∈ Submodule.span D (⋃ n, (γ n).baseChange D '' (torKer D J : Set (D ⊗[A] J)))
def

J

L298 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.J
Documentation

The extension of the ideal p0 to the R0-algebra A.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Stage
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
Lean source · statement
def J (A : Type*) [CommRing A] [Algebra R₀ A] : Ideal A
abbrev

T

L302 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.T
Documentation

The kernel of the extended ideal inclusion after base change from A to its tensor product with B0.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Stage
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
Lean source · statement
abbrev T (A : Type*) [CommRing A] [Algebra R₀ A] :
    Submodule (A ⊗[R₀] B₀) ((A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A))
def

Smon

L307 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Smon
Documentation

The image of the complement of p0 in the tensor product of A with B0.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Stage
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
Lean source · statement
def Smon [p₀.IsPrime] (A : Type*) [CommRing A] [Algebra R₀ A] : Submonoid (A ⊗[R₀] B₀)
theorem

isTorsionBySet_baseChange

L310 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.isTorsionBySet_baseChange
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Stage
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
Lean source · statement
theorem isTorsionBySet_baseChange [p₀.IsPrime] {Q : Type*} [AddCommGroup Q] [Module R₀ Q]
    (hQ : Module.IsTorsionBySet R₀ Q p₀) :
    Module.IsTorsionBySet (Localization.AtPrime p₀) (Localization.AtPrime p₀ ⊗[R₀] Q)
      (IsLocalRing.maximalIdeal (Localization.AtPrime p₀))
theorem

rTensor_ker_torsion

L330 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.rTensor_ker_torsion
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Stage
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
Lean source · statement
theorem rTensor_ker_torsion [p₀.IsPrime] {Q₁ Q₂ : Type*} [AddCommGroup Q₁] [AddCommGroup Q₂]
    [Module R₀ Q₁] [Module R₀ Q₂] (g : Q₁ →ₗ[R₀] Q₂) (hg : Function.Injective g)
    (h₂ : Module.IsTorsionBySet R₀ Q₂ p₀) (y : Q₁ ⊗[R₀] B₀) (hy : g.rTensor B₀ y = 0) :
    ∃ s ∈ p₀.primeCompl, s • y = 0
def

Φ

L377 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Φ
Documentation

The linear equivalence that exchanges the two tensor factors and cancels the intermediate scalar extension.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Stage
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable (A : Type u) [CommRing A] [Algebra R₀ A]
Lean source · statement
def Φ (Q : Type*) [AddCommGroup Q] [Module A Q] [Module R₀ Q] [IsScalarTower R₀ A Q] :
    (A ⊗[R₀] B₀) ⊗[A] Q ≃ₗ[A] Q ⊗[R₀] B₀
theorem

Φ_tmul

L381 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Φ_tmul
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Stage
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable (A : Type u) [CommRing A] [Algebra R₀ A]
Lean source · statement
theorem Φ_tmul {Q : Type*} [AddCommGroup Q] [Module A Q] [Module R₀ Q] [IsScalarTower R₀ A Q]
    (a : A) (b : B₀) (q : Q) : Φ B₀ A Q ((a ⊗ₜ[R₀] b) ⊗ₜ[A] q) = (a • q) ⊗ₜ[R₀] b
theorem

rel_torsion

L385 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.rel_torsion
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Stage
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable (A : Type u) [CommRing A] [Algebra R₀ A]
Lean source · statement
theorem rel_torsion [p₀.IsPrime] {Q₁ Q₂ : Type*} [AddCommGroup Q₁] [AddCommGroup Q₂]
    [Module A Q₁] [Module A Q₂] (g : Q₁ →ₗ[A] Q₂) (hg : Function.Injective g)
    (h₂ : Module.IsTorsionBySet A Q₂ (J p₀ A)) (x : (A ⊗[R₀] B₀) ⊗[A] Q₁)
    (hx : g.baseChange (A ⊗[R₀] B₀) x = 0) : ∃ s ∈ Smon B₀ p₀ A, s • x = 0
def

δ

L428 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.δ
Documentation

The tensor-product algebra map induced by h on the first factor and the identity on B0.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
def δ (h : A →ₐ[R₀] A') : A ⊗[R₀] B₀ →ₐ[R₀] A' ⊗[R₀] B₀
theorem

δ_tmul

L431 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.δ_tmul
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem δ_tmul (h : A →ₐ[R₀] A') (a : A) (b : B₀) :
    δ B₀ h (a ⊗ₜ[R₀] b) = h a ⊗ₜ[R₀] b
theorem

δ_comp

L434 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.δ_comp
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem δ_comp (h : A →ₐ[R₀] A') (h' : A' →ₐ[R₀] A'') (d : A ⊗[R₀] B₀) :
    δ B₀ h' (δ B₀ h d) = δ B₀ (h'.comp h) d
theorem

δ_smul

L440 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.δ_smul
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem δ_smul (h : A →ₐ[R₀] A') (a : A) (d : A ⊗[R₀] B₀) :
    δ B₀ h (a • d) = h a • δ B₀ h d
theorem

mem_J_map

L447 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.mem_J_map
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem mem_J_map (h : A →ₐ[R₀] A') {a : A} (ha : a ∈ J p₀ A) : h a ∈ J p₀ A'
def

ιJ

L457 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ιJ
Documentation

The R0-linear map between the extended ideals induced by h.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · full declaration
def ιJ (h : A →ₐ[R₀] A') : ↥(J p₀ A) →ₗ[R₀] ↥(J p₀ A') where
  toFun j := ⟨h j, mem_J_map p₀ h j.2⟩
  map_add' j j' := Subtype.ext (by simp)
  map_smul' r j := Subtype.ext (by simp [Algebra.smul_def])
theorem

coe_ιJ

L462 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.coe_ιJ
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem coe_ιJ (h : A →ₐ[R₀] A') (j : J p₀ A) : (ιJ p₀ h j : A') = h j
theorem

ιJ_comp

L464 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ιJ_comp
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem ιJ_comp (h : A →ₐ[R₀] A') (h' : A' →ₐ[R₀] A'') (j : J p₀ A) :
    ιJ p₀ h' (ιJ p₀ h j) = ιJ p₀ (h'.comp h) j
theorem

ιJ_injective

L467 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ιJ_injective
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem ιJ_injective (h : A →ₐ[R₀] A') (hh : Function.Injective h) :
    Function.Injective (ιJ p₀ h)
def

ξ

L476 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ξ
Documentation

The additive map on the tensors with extended ideals induced by the tensor-product map and the ideal map.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
def ξ (h : A →ₐ[R₀] A') :
    (A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A) →+ (A' ⊗[R₀] B₀) ⊗[A'] ↥(J p₀ A')
theorem

ξ_tmul

L490 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ξ_tmul
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem ξ_tmul (h : A →ₐ[R₀] A') (d : A ⊗[R₀] B₀) (j : J p₀ A) :
    ξ B₀ p₀ h (d ⊗ₜ[A] j) = δ B₀ h d ⊗ₜ[A'] ιJ p₀ h j
theorem

ξ_smul

L493 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ξ_smul
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem ξ_smul (h : A →ₐ[R₀] A') (c : A ⊗[R₀] B₀) (x : (A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A)) :
    ξ B₀ p₀ h (c • x) = δ B₀ h c • ξ B₀ p₀ h x
theorem

ξ_comp

L501 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ξ_comp
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
Lean source · statement
theorem ξ_comp (h : A →ₐ[R₀] A') (h' : A' →ₐ[R₀] A'') (x : (A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A)) :
    ξ B₀ p₀ h' (ξ B₀ p₀ h x) = ξ B₀ p₀ (h'.comp h) x
def

ρ

L510 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ρ
Documentation

The linear map sending a tensor of d with an element j of the extended ideal to j acting on d.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
Lean source · statement
def ρ : (A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A) →ₗ[A ⊗[R₀] B₀] A ⊗[R₀] B₀
theorem

ρ_tmul

L514 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ρ_tmul
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
Lean source · statement
theorem ρ_tmul (d : A ⊗[R₀] B₀) (j : J p₀ A) : ρ B₀ p₀ A (d ⊗ₜ[A] j) = (j :
  A) • d
theorem

mem_T_iff

L518 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.mem_T_iff
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
Lean source · statement
theorem mem_T_iff (x : (A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A)) : x ∈ T B₀ p₀ A ↔ ρ B₀ p₀ A x = 0
theorem

ρ_ξ

L522 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ρ_ξ
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
Lean source · statement
theorem ρ_ξ (h : A →ₐ[R₀] A') (x : (A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A)) :
    ρ B₀ p₀ A' (ξ B₀ p₀ h x) = δ B₀ h (ρ B₀ p₀ A x)
theorem

ξ_mem_T

L528 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ξ_mem_T
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
Lean source · statement
theorem ξ_mem_T (h : A →ₐ[R₀] A') {x : (A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A)} (hx : x ∈ T B₀ p₀ A) :
    ξ B₀ p₀ h x ∈ T B₀ p₀ A'
theorem

δ_mem_Smon

L533 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.δ_mem_Smon
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
Lean source · statement
theorem δ_mem_Smon [p₀.IsPrime] (h : A →ₐ[R₀] A') {s : A ⊗[R₀] B₀} (hs : s ∈ Smon B₀ p₀ A) :
    δ B₀ h s ∈ Smon B₀ p₀ A'
def

δA

L544 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.δA
Documentation

The A-algebra tensor-product map induced by scalar extension from A to A'.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
Lean source · statement
def δA : A ⊗[R₀] B₀ →ₐ[A] A' ⊗[R₀] B₀
theorem

δA_tmul

L547 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.δA_tmul
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
Lean source · statement
theorem δA_tmul (a : A) (b : B₀) :
    δA B₀ A A' (a ⊗ₜ[R₀] b) = algebraMap A A' a ⊗ₜ[R₀] b
theorem

δA_eq_δ

L550 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.δA_eq_δ
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
Lean source · statement
theorem δA_eq_δ (d : A ⊗[R₀] B₀) :
    δA B₀ A A' d = δ B₀ (IsScalarTower.toAlgHom R₀ A A') d
def

Θ

L559 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Θ
Documentation

The linear map on tensor products induced by extending the first factor from A to A'.

Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
variable (N' : Type*) [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
Lean source · statement
def Θ : (A ⊗[R₀] B₀) ⊗[A] N' →ₗ[A] (A' ⊗[R₀] B₀) ⊗[A'] N'
theorem

Θ_tmul

L572 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Θ_tmul
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
variable (N' : Type*) [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
variable {N'}
Lean source · statement
theorem Θ_tmul (d : A ⊗[R₀] B₀) (n : N') :
    Θ B₀ A A' N' (d ⊗ₜ[A] n) = δA B₀ A A' d ⊗ₜ[A'] n
theorem

Θ_smul

L576 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Θ_smul
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
variable (N' : Type*) [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
variable {N'}
Lean source · statement
theorem Θ_smul (c : A ⊗[R₀] B₀) (y : (A ⊗[R₀] B₀) ⊗[A] N') :
    Θ B₀ A A' N' (c • y) = δA B₀ A A' c • Θ B₀ A A' N' y
theorem

Θ_surjective

L584 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Θ_surjective
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
variable (N' : Type*) [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
variable {N'}
Lean source · statement
theorem Θ_surjective : Function.Surjective (Θ (R₀ := R₀) B₀ A A' N')
theorem

Θ_naturality

L602 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Θ_naturality
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
variable (N' : Type*) [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
variable {N'}
Lean source · statement
theorem Θ_naturality {N'' : Type*} [AddCommGroup N''] [Module A' N''] [Module A N'']
    [IsScalarTower A A' N''] (φ' : N' →ₗ[A'] N'') (y : (A ⊗[R₀] B₀) ⊗[A] N') :
    Θ B₀ A A' N'' ((φ'.restrictScalars A).baseChange (A ⊗[R₀] B₀) y) =
      (φ'.baseChange (A' ⊗[R₀] B₀)) (Θ B₀ A A' N' y)
theorem

Θ_span_le

L610 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Θ_span_le
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
variable (N' : Type*) [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
variable {N'}
Lean source · statement
theorem Θ_span_le (Z : Set ((A ⊗[R₀] B₀) ⊗[A] N')) {y : (A ⊗[R₀] B₀) ⊗[A] N'}
    (hy : y ∈ Submodule.span (A ⊗[R₀] B₀) Z) :
    Θ B₀ A A' N' y ∈ Submodule.span (A' ⊗[R₀] B₀) (Θ B₀ A A' N' '' Z)
theorem

Θ_injective_self

L619 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Θ_injective_self
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
section Theta
variable (A A')
variable [Algebra A A'] [IsScalarTower R₀ A A']
variable (N' : Type*) [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
variable {N'}
Lean source · statement
theorem Θ_injective_self : Function.Injective (Θ (R₀ := R₀) B₀ A A' A')
theorem

claim

L644 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.claim
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Transition
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀)
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
  {A'' : Type*} [CommRing A''] [Algebra R₀ A'']
variable (A) in
Lean source · statement
theorem claim [p₀.IsPrime] (h : A →ₐ[R₀] A') (x : (A' ⊗[R₀] B₀) ⊗[A'] ↥(J p₀ A'))
    (hx : x ∈ T B₀ p₀ A') :
    ∃ s ∈ Smon B₀ p₀ A', s • x ∈ Submodule.span (A' ⊗[R₀] B₀)
      (ξ B₀ p₀ h '' (T B₀ p₀ A : Set ((A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A))))
def

Ψ

L725 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Ψ
Documentation

The linear equivalence rewriting tensors with the extended ideal as the ideal tensored with B0.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
section RForm
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
variable (A) in
Lean source · statement
def Ψ : (A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A) ≃ₗ[A] ↥(J p₀ A) ⊗[R₀] B₀
theorem

Ψ_ξ

L727 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Ψ_ξ
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
section RForm
variable {A : Type*} [CommRing A] [Algebra R₀ A] {A' : Type*} [CommRing A'] [Algebra R₀ A']
variable (A) in
Lean source · statement
theorem Ψ_ξ (h : A →ₐ[R₀] A') (x : (A ⊗[R₀] B₀) ⊗[A] ↥(J p₀ A)) :
    Ψ B₀ p₀ A' (ξ B₀ p₀ h x) = (ιJ p₀ h).rTensor B₀ (Ψ B₀ p₀ A x)
def

JR

L745 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.JR
Documentation

The image of the ideal extended to E in the ideal extended to R.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
def JR (E : Subalgebra R₀ R) : Submodule R₀ ↥(J p₀ R)
theorem

ιJ_val_injective

L747 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.ιJ_val_injective
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem ιJ_val_injective (E : Subalgebra R₀ R) : Function.Injective (ιJ p₀ E.val)
theorem

JR_mono

L750 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.JR_mono
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem JR_mono {E E' : Subalgebra R₀ R} (hle : E ≤ E') : JR p₀ E ≤ JR p₀ E'
def

eJR

L755 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.eJR
Documentation

The linear equivalence from the extended ideal in E to its image in the extended ideal in R.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
def eJR (E : Subalgebra R₀ R) : ↥(J p₀ ↥E) ≃ₗ[R₀] ↥(JR p₀ E)
theorem

coe_eJR

L758 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.coe_eJR
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem coe_eJR (E : Subalgebra R₀ R) (j : J p₀ ↥E) :
    ((eJR p₀ E j : ↥(JR p₀ E)) : ↥(J p₀ R)) = ιJ p₀ E.val j
theorem

subtype_comp_eJR

L762 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.subtype_comp_eJR
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem subtype_comp_eJR (E : Subalgebra R₀ R) :
    (JR p₀ E).subtype ∘ₗ (eJR p₀ E : ↥(J p₀ ↥E) →ₗ[R₀] ↥(JR p₀ E)) = ιJ p₀ E.val
theorem

val_comp_inclusion

L766 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.val_comp_inclusion
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem val_comp_inclusion {E E' : Subalgebra R₀ R} (hle : E ≤ E') :
    E'.val.comp (Subalgebra.inclusion hle) = E.val
theorem

inclusion_comp_inclusion

L769 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.inclusion_comp_inclusion
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem inclusion_comp_inclusion {E E' E'' : Subalgebra R₀ R} (h₁ : E ≤ E') (h₂ : E' ≤ E'') :
    (Subalgebra.inclusion h₂).comp (Subalgebra.inclusion h₁) = Subalgebra.inclusion (h₁.trans h₂)
theorem

exists_fg_mem_JR

L773 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.exists_fg_mem_JR
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem exists_fg_mem_JR (g : J p₀ R) : ∃ E : Subalgebra R₀ R, E.FG ∧ g ∈ JR p₀ E
theorem

exists_fg_le_JR

L803 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.exists_fg_le_JR
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem exists_fg_le_JR (E₀ : Subalgebra R₀ R) (hE₀ : E₀.FG) (N : Submodule R₀ ↥(J p₀ R))
    (hN : N.FG) : ∃ E : Subalgebra R₀ R, E₀ ≤ E ∧ E.FG ∧ N ≤ JR p₀ E
theorem

exists_fg_ξ_eq_zero

L819 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.exists_fg_ξ_eq_zero
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem exists_fg_ξ_eq_zero (E : Subalgebra R₀ R) (hE : E.FG)
    (z : (↥E ⊗[R₀] B₀) ⊗[↥E] ↥(J p₀ ↥E)) (hz : ξ B₀ p₀ E.val z = 0) :
    ∃ E' : Subalgebra R₀ R, ∃ hle : E ≤ E', E'.FG ∧
      ξ B₀ p₀ (Subalgebra.inclusion hle) z = 0
theorem

exists_fg_mem_range_δ

L856 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.exists_fg_mem_range_δ
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem exists_fg_mem_range_δ (b : R ⊗[R₀] B₀) :
    ∃ E : Subalgebra R₀ R, E.FG ∧ b ∈ Set.range (δ B₀ E.val)
theorem

torsion_of_mem_span

L869 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.torsion_of_mem_span
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem torsion_of_mem_span {D X : Type*} [CommRing D] [AddCommGroup X] [Module D X]
    (Q : Ideal D) [hQ : Q.IsPrime] (S : Set X) (hS : ∀ y ∈ S, ∃ c ∉ Q, c • y = 0) {x : X}
    (hx : x ∈ Submodule.span D S) : ∃ c ∉ Q, c • x = 0
theorem

map_mem_span_image

L886 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.map_mem_span_image
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
Lean source · statement
theorem map_mem_span_image {D₀ D X₀ X : Type*} [CommRing D₀] [CommRing D] [AddCommGroup X₀]
    [Module D₀ X₀] [AddCommGroup X] [Module D X] (δ' : D₀ → D) (ψ : X₀ →+ X)
    (hψ : ∀ (c : D₀) (x : X₀), ψ (c • x) = δ' c • ψ x) (S : Set X₀) {t : X₀}
    (ht : t ∈ Submodule.span D₀ S) : ψ t ∈ Submodule.span D (ψ '' S)
def

Tors

L902 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Tors
Documentation

The image of t at the subalgebra stage E is annihilated by an element outside the contraction of P.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
variable (P : Ideal (R ⊗[R₀] B₀))
local notation "Rb" => (⊥ : Subalgebra R₀ R)
Lean source · statement
def Tors (E : Subalgebra R₀ R) (t : (↥Rb ⊗[R₀] B₀) ⊗[↥Rb]
    ↥(J p₀ ↥Rb)) : Prop
theorem

mono

L906 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Tors.mono
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
variable (P : Ideal (R ⊗[R₀] B₀))
local notation "Rb" => (⊥ : Subalgebra R₀ R)
Lean source · statement
theorem Tors.mono {E E' : Subalgebra R₀ R} (hle : E ≤ E') {t} (ht : Tors B₀ p₀ P E t) :
    Tors B₀ p₀ P E' t
theorem

exists_fg_tors

L914 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.exists_fg_tors
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
variable (P : Ideal (R ⊗[R₀] B₀))
local notation "Rb" => (⊥ : Subalgebra R₀ R)
Lean source · statement
theorem exists_fg_tors (htop : ∀ x ∈ T B₀ p₀ R, ∃ b ∉ P, b • x = 0)
    (t : (↥Rb ⊗[R₀] B₀) ⊗[↥Rb]
      ↥(J p₀ ↥Rb)) (ht : t ∈ T B₀ p₀ ↥Rb) :
    ∃ E : Subalgebra R₀ R, E.FG ∧ Tors B₀ p₀ P E t
theorem

Smon_disjoint

L929 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.Smon_disjoint
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
variable (P : Ideal (R ⊗[R₀] B₀))
local notation "Rb" => (⊥ : Subalgebra R₀ R)
Lean source · statement
theorem Smon_disjoint [p₀.IsPrime] (hP : P.comap (algebraMap R₀ (R ⊗[R₀] B₀)) = p₀)
    (E : Subalgebra R₀ R) {s : ↥E ⊗[R₀] B₀} (hs : s ∈ Smon B₀ p₀ ↥E) :
    s ∉ P.comap (δ B₀ E.val)
theorem

exists_fg_T_torsion

L937 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.exists_fg_T_torsion
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Descent
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) {R : Type*} [CommRing R] [Algebra R₀ R]
variable (P : Ideal (R ⊗[R₀] B₀))
local notation "Rb" => (⊥ : Subalgebra R₀ R)
Lean source · statement
theorem exists_fg_T_torsion [IsNoetherianRing R₀] [Algebra.FiniteType R₀ B₀] [p₀.IsPrime]
    [P.IsPrime]
    (hP : P.comap (algebraMap R₀ (R ⊗[R₀] B₀)) = p₀)
    (htop : ∀ x ∈ T B₀ p₀ R, ∃ b ∉ P, b • x = 0) :
    ∃ E : Subalgebra R₀ R, E.FG ∧
      ∀ x ∈ T B₀ p₀ ↥E, ∃ c ∉ P.comap (δ B₀ E.val), c • x = 0
theorem

cancelBaseChange_lTensor_baseChange

L990 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.cancelBaseChange_lTensor_baseChange
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Endgame
Lean source · statement
theorem cancelBaseChange_lTensor_baseChange {A D M' : Type*} [CommRing A] [CommRing D]
    [CommRing M'] [Algebra A D] [Algebra D M'] [Algebra A M'] [IsScalarTower A D M']
    {N N'' : Type*} [AddCommGroup N] [Module A N] [AddCommGroup N''] [Module A N'']
    (f : N →ₗ[A] N'') (z : M' ⊗[D] (D ⊗[A] N)) :
    TensorProduct.AlgebraTensorModule.cancelBaseChange A D M' M' N''
        ((f.baseChange D).lTensor M' z) =
      f.lTensor M' (TensorProduct.AlgebraTensorModule.cancelBaseChange A D M' M' N z)
theorem

lTensor_localization_injective

L1004 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.lTensor_localization_injective
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Endgame
Lean source · statement
theorem lTensor_localization_injective {A D : Type*} [CommRing A] [CommRing D] [Algebra A D]
    (P : Ideal D) [P.IsPrime] {N N'' : Type*} [AddCommGroup N] [Module A N] [AddCommGroup N'']
    [Module A N''] (f : N →ₗ[A] N'')
    (htor : ∀ z, f.baseChange D z = 0 → ∃ c ∉ P, c • z = 0) :
    Function.Injective (f.lTensor (Localization.AtPrime P))
theorem

flat_localization_of_T_torsion

L1043 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.flat_localization_of_T_torsion
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Endgame
variable {R₀ : Type*} [CommRing R₀] (B₀ : Type*) [CommRing B₀] [Algebra R₀ B₀]
  (p₀ : Ideal R₀) (A : Type u) [CommRing A] [Algebra R₀ A]
Lean source · statement
theorem flat_localization_of_T_torsion [p₀.IsPrime] [IsNoetherianRing A]
    [IsNoetherianRing (A ⊗[R₀] B₀)] (P₁ : Ideal (A ⊗[R₀] B₀)) [P₁.IsPrime]
    (hP₁ : P₁.comap (algebraMap R₀ (A ⊗[R₀] B₀)) = p₀)
    (htor : ∀ x ∈ T B₀ p₀ A, ∃ c ∉ P₁, c • x = 0) :
    Module.Flat A (Localization.AtPrime P₁)
theorem

torsion_of_flat_localization

L1093 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.torsion_of_flat_localization
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Main
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]
Lean source · statement
theorem torsion_of_flat_localization {A D : Type*} [CommRing A] [CommRing D] [Algebra A D]
    (P : Ideal D) [P.IsPrime] [Module.Flat A (Localization.AtPrime P)]
    {N N'' : Type*} [AddCommGroup N] [Module A N] [AddCommGroup N''] [Module A N'']
    (f : N →ₗ[A] N'') (hf : Function.Injective f) (x : D ⊗[A] N)
    (hx : f.baseChange D x = 0) : ∃ b ∉ P, b • x = 0
theorem

T_top_torsion

L1113 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct.FlatDescentFG.T_top_torsion
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
noncomputable section
namespace FlatDescentFG
universe u v w
open scoped FreeCover
section Main
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]
Lean source · statement
theorem T_top_torsion (P : Ideal (R ⊗[R₀] B₀)) [P.IsPrime]
    [Module.Flat R (Localization.AtPrime P)] (p₀ : Ideal R₀) (x : (R ⊗[R₀] B₀) ⊗[R] ↥(J p₀ R))
    (hx : x ∈ T B₀ p₀ R) : ∃ b ∉ P, b • x = 0
theorem

exists_fg_subalgebra_flat_localization_tensorProduct

L1126 ↗
Module.Flat.exists_fg_subalgebra_flat_localization_tensorProduct
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
open TensorProduct LinearMap
open FlatDescentFG in
Lean source · statement
theorem _root_.Module.Flat.exists_fg_subalgebra_flat_localization_tensorProduct
    {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀]
    [Algebra R₀ R] [Algebra R₀ B₀] [IsNoetherianRing R₀] [Algebra.FiniteType R₀ B₀]
    (P : Ideal (R ⊗[R₀] B₀)) [P.IsPrime]
    [Module.Flat R (Localization.AtPrime P)] :
    ∃ R₁ : Subalgebra R₀ R, R₁.FG ∧
      Module.Flat R₁ (Localization.AtPrime
        (P.comap (Algebra.TensorProduct.map R₁.val (AlgHom.id R₀ B₀)).toRingHom))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.