Module

QuotientBaseChange.lean

Nyll.SchemeTheory.RingTheory.QuotientBaseChange

4 declarations indexed from sourceView source ↗

Module documentation

Algebra maps on reduction modulo a base ideal

The map between the quotients by the extended base ideal is an algebra map over the quotient base. The quotient/tensor equivalences identify it with the canonical tensor-product base change.

Imports5

Mathlib.Algebra.Algebra.Tower
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.TensorProduct.Maps
Mathlib.RingTheory.TensorProduct.Quotient

Imported by8

theorem

map_extendedIdeal

AlgHom.map_extendedIdeal

Documentation

An algebra map carries the ideal extended from the base to the corresponding extended ideal in the target.

Source context 5 commands

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

@[expose] public section
open scoped TensorProduct
universe u v w
namespace AlgHom
variable {R : Type u} {A : Type v} {B : Type w}
  [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]

Lean source · statement

theorem map_extendedIdeal (f : A →ₐ[R] B) (I : Ideal R) :
    (I.map (algebraMap R A)).map f.toRingHom = I.map (algebraMap R B)

def

quotientBaseChange

AlgHom.quotientBaseChange

Documentation

The quotient-base algebra map induced by an algebra map.

Source context 5 commands

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

@[expose] public section
open scoped TensorProduct
universe u v w
namespace AlgHom
variable {R : Type u} {A : Type v} {B : Type w}
  [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]

Lean source · statement

def quotientBaseChange (f : A →ₐ[R] B) (I : Ideal R) :
    A ⧸ I.map (algebraMap R A) →ₐ[R ⧸ I] B ⧸ I.map (algebraMap R B)

theorem

quotientBaseChange_mk

AlgHom.quotientBaseChange_mk

Source context 5 commands

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

@[expose] public section
open scoped TensorProduct
universe u v w
namespace AlgHom
variable {R : Type u} {A : Type v} {B : Type w}
  [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]

Lean source · statement

theorem quotientBaseChange_mk (f : A →ₐ[R] B) (I : Ideal R) (a : A) :
    f.quotientBaseChange I (Ideal.Quotient.mk (I.map (algebraMap R A)) a) =
      Ideal.Quotient.mk (I.map (algebraMap R B)) (f a)

theorem

quotientBaseChange_tensorProduct

AlgHom.quotientBaseChange_tensorProduct

Documentation

The concrete quotient map agrees with tensor-product base change under the canonical quotient/tensor comparisons.

Source context 5 commands

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

@[expose] public section
open scoped TensorProduct
universe u v w
namespace AlgHom
variable {R : Type u} {A : Type v} {B : Type w}
  [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]

Lean source · statement

theorem quotientBaseChange_tensorProduct (f : A →ₐ[R] B) (I : Ideal R) :
    (Algebra.TensorProduct.quotIdealMapEquivQuotTensor B I).toAlgHom.comp
        (f.quotientBaseChange I) =
      (Algebra.TensorProduct.map (.id (R ⧸ I) (R ⧸ I)) f).comp
        (Algebra.TensorProduct.quotIdealMapEquivQuotTensor A I).toAlgHom