noncomputable def module_inst (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] (f : B →ₐ[K] A) : Type u

Equations

• module_inst K A B M f = M

noncomputable instance instAddCommGroupModule_inst (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] (f : B →ₐ[K] A) [AddCommGroup M] : AddCommGroup (module_inst K A B M f)

Equations

• instAddCommGroupModule_inst K A B M f = inferInstanceAs (AddCommGroup M)

noncomputable instance inst_K_mod (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : Module K (module_inst K A B M f)

Equations

• inst_K_mod K A B M f = Module.compHom M (algebraMap K A)

noncomputable instance instModuleModule_instOfIsScalarTowerOfIsSimpleModule (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : Module A (module_inst K A B M f)

Equations

• instModuleModule_instOfIsScalarTowerOfIsSimpleModule K A B M f = inferInstanceAs (Module A M)

instance instIsScalarTowerModule_inst (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : IsScalarTower K A (module_inst K A B M f)

noncomputable def smul1AddHom' (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : module_inst K A B M f → B →+ Module.End A M →+ module_inst K A B M f

Equations

• smul1AddHom' K A B M f m = { toFun := fun (b : B) => { toFun := fun (l : Module.End A M) => f b • l m, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def smul1AddHom (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : module_inst K A B M f → TensorProduct K B (Module.End A M) →+ module_inst K A B M f

Equations

• smul1AddHom K A B M f m = TensorProduct.liftAddHom (smul1AddHom' K A B M f m) ⋯

noncomputable def smul1 (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : module_inst K A B M f → TensorProduct K B (Module.End A M) →ₗ[K] module_inst K A B M f

Equations

• smul1 K A B M f m = { toFun := (↑(smul1AddHom K A B M f m)).toFun, map_add' := ⋯, map_smul' := ⋯ }

theorem one_smul1 (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) (m : module_inst K A B M f) : (smul1 K A B M f m) 1 = m

theorem mul_smul1 (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) (x y : TensorProduct K B (Module.End A M)) (m : module_inst K A B M f) : (smul1 K A B M f m) (x * y) = (smul1 K A B M f ((smul1 K A B M f m) y)) x

theorem smul1_add (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) (r : TensorProduct K B (Module.End A M)) (m1 m2 : module_inst K A B M f) : (smul1 K A B M f (m1 + m2)) r = (smul1 K A B M f m1) r + (smul1 K A B M f m2) r

theorem add_smul1 (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) (r s : TensorProduct K B (Module.End A M)) (x : module_inst K A B M f) : (smul1 K A B M f x) (r + s) = (smul1 K A B M f x) r + (smul1 K A B M f x) s

noncomputable instance IsMod (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : Module (TensorProduct K B (Module.End A M)) (module_inst K A B M f)

Equations

• IsMod K A B M f = Module.mk ⋯ ⋯

instance instIsScalarTowerTensorProductEndModule_inst (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : IsScalarTower K (TensorProduct K B (Module.End A M)) (module_inst K A B M f)

instance module_inst_findim (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : Module.Finite (TensorProduct K B (Module.End A M)) (module_inst K A B M f)

instance tensor_is_simple (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B] [IsSimpleRing B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] [Algebra.IsCentral K A] [csa_A : IsSimpleRing A] : IsSimpleRing (TensorProduct K B (Module.End A M))

theorem findimB (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Algebra.IsCentral K A] [IsSimpleRing A] [Ring B] [Algebra K B] [hB : IsSimpleRing B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f : B →ₐ[K] A) : FiniteDimensional K B

theorem iso_fg (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Algebra.IsCentral K A] [IsSimpleRing A] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f g : B →ₐ[K] A) [hB1 : IsSimpleRing B] : Nonempty (module_inst K A B M f ≃ₗ[TensorProduct K B (Module.End A M)] module_inst K A B M g)

theorem SkolemNoether (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Algebra.IsCentral K A] [IsSimpleRing A] [Ring B] [Algebra K B] [hB : IsSimpleRing B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] [IsSimpleModule A M] (f g : B →ₐ[K] A) : ∃ (x : Aˣ), ∀ (b : B), g b = ↑x * f b * ↑x⁻¹

End_End_A

theorem SkolemNoether' (K A B : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Algebra.IsCentral K A] [IsSimpleRing A] [Ring B] [Algebra K B] [hB : IsSimpleRing B] (f g : B →ₐ[K] A) : ∃ (x : Aˣ), ∀ (b : B), g b = ↑x * f b * ↑x⁻¹