Module

Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight

6 declarations indexed from sourceView source ↗

Module documentation

Algebra, divisors, and base change

Equality of the two tensor-square images is the descent condition for an ideal along a faithfully flat algebra.

Imports2

Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Mathlib.RingTheory.TensorProduct.Basic

Imported by2

def

DescentCondition

L39 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight.Ideal.DescentCondition

Documentation

The two tensor inclusions send the ideal to the same ideal of the tensor square.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight
universe u
open TensorProduct
namespace Ideal
open _root_.Ideal
open _root_.Ideal
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

def DescentCondition (I : Ideal B) : Prop

theorem

map_comap_eq_self_of_descentCondition_of_section

L43 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight.Ideal.map_comap_eq_self_of_descentCondition_of_section

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight
universe u
open TensorProduct
namespace Ideal
open _root_.Ideal
open _root_.Ideal
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem map_comap_eq_self_of_descentCondition_of_section (σ : B →ₐ[A] A) (I : Ideal B)
    (hI : DescentCondition (A := A) I) :
    (I.comap (algebraMap A B)).map (algebraMap A B) = I

theorem

descentCondition_map

L92 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight.Ideal.descentCondition_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight
universe u
open TensorProduct
namespace Ideal
open _root_.Ideal
open _root_.Ideal
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem descentCondition_map (I₀ : Ideal A) : DescentCondition (A := A) (I₀.map
  (algebraMap A B))

theorem

comap_includeLeft_map_includeRight

L101 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight.Ideal.comap_includeLeft_map_includeRight

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight
universe u
open TensorProduct
namespace Ideal
open _root_.Ideal
open _root_.Ideal
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem comap_includeLeft_map_includeRight [Module.Flat A B] (I : Ideal B) :
    (I.map ((Algebra.TensorProduct.includeRight : B →ₐ[A] B ⊗[A] B) : B →+* B ⊗[A] B)).comap
        (Algebra.TensorProduct.includeLeftRingHom : B →+* B ⊗[A] B) =
      (I.comap (algebraMap A B)).map (algebraMap A B)

theorem

map_comap_eq_self_of_descentCondition

L146 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight.Ideal.map_comap_eq_self_of_descentCondition

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight
universe u
open TensorProduct
namespace Ideal
open _root_.Ideal
open _root_.Ideal
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem map_comap_eq_self_of_descentCondition [Module.FaithfullyFlat A B] (I : Ideal B)
    (hI : DescentCondition (A := A) I) :
    (I.comap (algebraMap A B)).map (algebraMap A B) = I

theorem

map_comap_eq_self_of_map_includeLeft_eq_map_includeRight

L189 ↗

Ideal.map_comap_eq_self_of_map_includeLeft_eq_map_includeRight

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight
universe u
open TensorProduct

Lean source · statement

theorem _root_.Ideal.map_comap_eq_self_of_map_includeLeft_eq_map_includeRight
    {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B]
    (I : Ideal B)
    (hI : I.map (Algebra.TensorProduct.includeLeftRingHom : B →+* B ⊗[A] B) =
      I.map ((Algebra.TensorProduct.includeRight : B →ₐ[A] B ⊗[A] B) : B →+* B ⊗[A] B)) :
    (I.comap (algebraMap A B)).map (algebraMap A B) = I

Module documentation

Algebra, divisors, and base change

Declarations

DescentCondition

map_comap_eq_self_of_descentCondition_of_section

descentCondition_map

comap_includeLeft_map_includeRight

map_comap_eq_self_of_descentCondition

map_comap_eq_self_of_map_includeLeft_eq_map_includeRight