NYLL
Module

IdempotentFactorReduction.lean

Nyll.SchemeTheory.RingTheory.IdempotentFactorReduction
7 declarations indexed from sourceView source ↗

Module documentation

Reduction of an idempotent factor

Imposing e = 1 commutes with reducing by an extended base ideal. The comparison is obtained from the canonical interchange of two quotient rings. It also identifies a reduced factor with a specified factor of a product.

Imports7
  • Nyll.SchemeTheory.RingTheory.QuotientBaseChange
  • Mathlib.Algebra.Algebra.Prod
  • Mathlib.Algebra.Algebra.Tower
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.Ideal.Over
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.RingTheory.Ideal.Span
Imported by2

Declarations

def

idempotentFactorReduction

L35 ↗
Algebra.idempotentFactorReduction
Documentation

Taking the factor where e = 1 commutes with reduction modulo the base ideal. The construction does not require idempotence of e.

Source context 4 commands

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

@[expose] public noncomputable section
universe u v w z
namespace Algebra
variable {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
Lean source · statement
def idempotentFactorReduction (I : Ideal R) (e : C) :
    ((C ⧸ Ideal.span {1 - e}) ⧸
      I.map (algebraMap R (C ⧸ Ideal.span {1 - e}))) ≃ₐ[R ⧸ I]
    (C ⧸ I.map (algebraMap R C)) ⧸
      Ideal.span {1 - Ideal.Quotient.mk (I.map (algebraMap R C)) e}
theorem

idempotentFactorReduction_mk_mk

L57 ↗
Algebra.idempotentFactorReduction_mk_mk
Source context 4 commands

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

@[expose] public noncomputable section
universe u v w z
namespace Algebra
variable {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
Lean source · statement
theorem idempotentFactorReduction_mk_mk (I : Ideal R) (e c : C) :
    idempotentFactorReduction I e
      (Ideal.Quotient.mk _ (Ideal.Quotient.mk (Ideal.span {1 - e}) c)) =
        Ideal.Quotient.mk _ (Ideal.Quotient.mk (I.map (algebraMap R C)) c)
def

idempotentFactorReductionEquivOfEqOne

L64 ↗
Algebra.idempotentFactorReductionEquivOfEqOne
Documentation

If e reduces to 1, its factor has the same reduction as the original algebra.

Source context 4 commands

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

@[expose] public noncomputable section
universe u v w z
namespace Algebra
variable {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
Lean source · statement
def idempotentFactorReductionEquivOfEqOne (I : Ideal R) (e : C)
    (he : Ideal.Quotient.mk (I.map (algebraMap R C)) e = 1) :
    ((C ⧸ Ideal.span {1 - e}) ⧸
      I.map (algebraMap R (C ⧸ Ideal.span {1 - e}))) ≃ₐ[R ⧸ I]
        C ⧸ I.map (algebraMap R C)
theorem

idempotentFactorReductionEquivOfEqOne_mk_mk

L77 ↗
Algebra.idempotentFactorReductionEquivOfEqOne_mk_mk
Source context 4 commands

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

@[expose] public noncomputable section
universe u v w z
namespace Algebra
variable {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
Lean source · statement
theorem idempotentFactorReductionEquivOfEqOne_mk_mk
    (I : Ideal R) (e : C)
    (he : Ideal.Quotient.mk (I.map (algebraMap R C)) e = 1) (c : C) :
    idempotentFactorReductionEquivOfEqOne I e he
      (Ideal.Quotient.mk _ (Ideal.Quotient.mk (Ideal.span {1 - e}) c)) =
        Ideal.Quotient.mk (I.map (algebraMap R C)) c
def

quotientOneSubEquivFst

L86 ↗
Algebra.quotientOneSubEquivFst
Documentation

A product decomposition sending e to (1, 0) identifies the quotient by 1 - e with the first factor.

Source context 4 commands

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

@[expose] public noncomputable section
universe u v w z
namespace Algebra
variable {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
Lean source · statement
def quotientOneSubEquivFst
    {Q : Type u} {A : Type v} {D : Type w} {F : Type z}
    [CommRing Q] [CommRing A] [CommRing D] [CommRing F]
    [Algebra Q A] [Algebra Q D] [Algebra Q F]
    (E : A ≃ₐ[Q] D × F) (e : A) (he : E e = (1, 0)) :
    (A ⧸ Ideal.span {1 - e}) ≃ₐ[Q] D
def

idempotentFactorReductionEquivFst

L123 ↗
Algebra.idempotentFactorReductionEquivFst
Documentation

A product decomposition of the reduction identifies the reduced factor selected by (1, 0) with its first factor.

Source context 4 commands

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

@[expose] public noncomputable section
universe u v w z
namespace Algebra
variable {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
Lean source · statement
def idempotentFactorReductionEquivFst (I : Ideal R) (e : C)
    {D : Type w} {F : Type z} [CommRing D] [CommRing F]
    [Algebra (R ⧸ I) D] [Algebra (R ⧸ I) F]
    (E : (C ⧸ I.map (algebraMap R C)) ≃ₐ[R ⧸ I] D × F)
    (hE : E (Ideal.Quotient.mk (I.map (algebraMap R C)) e) = (1, 0)) :
    ((C ⧸ Ideal.span {1 - e}) ⧸
      I.map (algebraMap R (C ⧸ Ideal.span {1 - e}))) ≃ₐ[R ⧸ I] D
theorem

idempotentFactorReductionEquivFst_mk_mk

L134 ↗
Algebra.idempotentFactorReductionEquivFst_mk_mk
Source context 4 commands

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

@[expose] public noncomputable section
universe u v w z
namespace Algebra
variable {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
Lean source · statement
theorem idempotentFactorReductionEquivFst_mk_mk (I : Ideal R) (e : C)
    {D : Type w} {F : Type z} [CommRing D] [CommRing F]
    [Algebra (R ⧸ I) D] [Algebra (R ⧸ I) F]
    (E : (C ⧸ I.map (algebraMap R C)) ≃ₐ[R ⧸ I] D × F)
    (hE : E (Ideal.Quotient.mk (I.map (algebraMap R C)) e) = (1, 0)) (c : C) :
    idempotentFactorReductionEquivFst I e E hE
      (Ideal.Quotient.mk _ (Ideal.Quotient.mk (Ideal.span {1 - e}) c)) =
        (E (Ideal.Quotient.mk (I.map (algebraMap R C)) c)).1

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