LeanPool.BrauerGroupNew.Mathlib.RingTheory.Congruence.Basic

Imported Lean Pool material for LeanPool.BrauerGroupNew.Mathlib.RingTheory.Congruence.Basic.

Ring congruence quotient compatibility

This file restores the upstream quotient-map names used by the Brauer group port.

@[implicit_reducible]

instance RingCon.instModuleQuotientOfIsScalarTowerLeanPool {α : Type u_1} {R : Type u_2} [Semiring α] [NonAssocSemiring R] [Module α R] [IsScalarTower α R R] (c : RingCon R) : Module α c.Quotient

Equations

• c.instModuleQuotientOfIsScalarTowerLeanPool = { toDistribMulAction := c.instDistribMulActionQuotientOfIsScalarTower, add_smul := ⋯, zero_smul := ⋯ }

def RingCon.mkL (α : Type u_1) {R : Type u_2} [Semiring α] [NonAssocSemiring R] [Module α R] [IsScalarTower α R R] (c : RingCon R) : R →ₗ[α] c.Quotient

The quotient map as a linear map.

Equations

• RingCon.mkL α c = { toFun := (↑↑c.mk').toFun, map_add' := ⋯, map_smul' := ⋯ }

theorem RingCon.algebraMap_def {α : Type u_1} {R : Type u_2} [CommSemiring α] [Semiring R] [Algebra α R] (c : RingCon R) : algebraMap α c.Quotient = c.mk'.comp (algebraMap α R)

def RingCon.mkA (α : Type u_1) {R : Type u_2} [CommSemiring α] [Semiring R] [Algebra α R] (c : RingCon R) : R →ₐ[α] c.Quotient

The quotient map as an algebra homomorphism.

Equations

• RingCon.mkA α c = RingCon.mkₐ α c