LeanPool.BrauerGroupNew.SkolemNoether

Imported Lean Pool material for LeanPool.BrauerGroupNew.SkolemNoether.

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

Type synonym for viewing an A-module through an embedding of B into A.

Equations

• moduleInst K A B M f = (fun (x : B →ₐ[K] A) => M) f

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance instKMod (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module A M] (f : B →ₐ[K] A) : Module K (moduleInst K A B M f)

Equations

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

@[implicit_reducible]

noncomputable instance instModuleModuleInst (K A B M : Type u) [Field K] [Ring A] [Algebra K A] [Ring B] [Algebra K B] [AddCommGroup M] [Module A M] (f : B →ₐ[K] A) : Module A (moduleInst K A B M f)

Equations

• instModuleModuleInst K A B M f = { toSMul := instModuleModuleInst._aux_1 K A B M f, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

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

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

The additive action map before tensor-product descent.

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] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] (f : B →ₐ[K] A) : moduleInst K A B M f → TensorProduct K B (Module.End A M) →+ moduleInst K A B M f

The tensor-product additive action on the transported module.

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] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] (f : B →ₐ[K] A) : moduleInst K A B M f → TensorProduct K B (Module.End A M) →ₗ[K] moduleInst K A B M f

The tensor-product linear action on the transported module.

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] (f : B →ₐ[K] A) (m : moduleInst 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] (f : B →ₐ[K] A) (x y : TensorProduct K B (Module.End A M)) (m : moduleInst 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] (f : B →ₐ[K] A) (r : TensorProduct K B (Module.End A M)) (m1 m2 : moduleInst 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] (f : B →ₐ[K] A) (r s : TensorProduct K B (Module.End A M)) (x : moduleInst 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

@[implicit_reducible]

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] (f : B →ₐ[K] A) : Module (TensorProduct K B (Module.End A M)) (moduleInst K A B M f)

Equations

• One or more equations did not get rendered due to their size.

instance instIsScalarTowerTensorProductEndModuleInstOfIsSimpleModule (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)) (moduleInst K A B M f)

instance moduleInst_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)) (moduleInst 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 (moduleInst K A B M f ≃ₗ[TensorProduct K B (Module.End A M)] moduleInst 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⁻¹