OAI/Algebra/Finitistic/Dimension/PDBalancedRight.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PDTensor.mapRight line 15
2. theorem OAI.LittleFinitistic.PDTensor.mapRight_mk line 24
3. theorem OAI.LittleFinitistic.PDTensor.mk_radical_zero line 31

   Source documentation

   Radical multiplication is killed by tensor with any right module annihilated by the ring radical.

   theorem mk_radical_zero
       (hU : ∀ a ∈ Ring.jacobson A, ∀ u : U, MulOpposite.op a • u = 0)
       (n : N) (hn : n ∈ Ring.jacobson A • (⊤ : Submodule A N)) (u : U) :
       BalancedTensor.mk k A U N u n = 0 := by
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.mk

4. theorem OAI.LittleFinitistic.PDTensor.mapRight_radical_zero line 47
5. def OAI.LittleFinitistic.PDTensor.rightRadical line 57

   Source documentation

   The actual right radical quotient of the regular module.

   def rightRadical : Submodule Aᵐᵒᵖ A where
   …

6. abbrev OAI.LittleFinitistic.PDTensor.Residue line 63
7. theorem OAI.LittleFinitistic.PDTensor.residue_annihilated line 65