FLT/Mathlib/RingTheory/SimpleRing/TensorProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Tensor product of simple algebras over a field

In this file, we show that the tensor product of a simple algebra and a central simple algebra is simple, which in particular implies that the tensor product of two central simple algebras is another central simple algebra. This is a prerequisite for defining the group law on the Brauer group.

Main Results

References

Tags

Noncommutative algebra, tensor product, simple algebra, central simple algebra

Imports (8)
Imported by 2 files
  1. lemma TwoSidedIdeal.span_eq_bot line 50 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: NonUnitalNonAssocRing, Set, Iff, Eq, TwoSidedIdeal, TwoSidedIdeal.span, Bot.bot, Membership.mem, OfNat.ofNat

    Proof uses: Iff.trans, LE.le, eq_bot_iff, Iff.intro, Iff.mp, TwoSidedIdeal.mem_bot, TwoSidedIdeal.subset_span, Iff.mpr, TwoSidedIdeal.span_le

    23 instances, coercions and auxiliary constants left out.

  2. lemma TwoSidedIdeal.span_singleton_eq_bot line 55 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: NonUnitalNonAssocRing, Iff, Eq, TwoSidedIdeal, TwoSidedIdeal.span, Singleton.singleton, Set, Bot.bot, OfNat.ofNat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, forall_congr, implies_congr, Eq.refl, iff_self

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  3. lemma TwoSidedIdeal.map_bot line 58 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NonUnitalNonAssocRing, FunLike, ZeroHomClass, Eq, TwoSidedIdeal, TwoSidedIdeal.map, Bot.bot

    Proof uses: TwoSidedIdeal.ext, of_eq_true, Iff, Membership.mem, Eq.trans, OfNat.ofNat, True, congr, congrArg, congrFun', TwoSidedIdeal.span, Set.image, Singleton.singleton, Set, Set.image_singleton, map_zero, Iff.mpr, TwoSidedIdeal.span_singleton_eq_bot, eq_self, iff_self

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  4. theorem TwoSidedIdeal.mem_map_of_mem line 65 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: NonUnitalNonAssocRing, FunLike, TwoSidedIdeal, Membership.mem, TwoSidedIdeal.map

    Proof uses: TwoSidedIdeal.subset_span, Set.image, Exists.intro, And, Set, Eq, And.intro, rfl

    8 instances, coercions and auxiliary constants left out.

  5. theorem Submodule.mem_span_range_iff_exists line 73 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Semiring, AddCommMonoid, Module, Iff, Membership.mem, Submodule, Submodule.span, Set.range, Exists, Finset, Eq, Finset.sum, HSMul.hSMul

    Proof uses: Eq.mpr, Set.image, Set.univ, id, congrArg, Set, Eq.symm, Set.image_univ, And, LE.le, Subtype, Finset.univ, propext, Submodule.mem_span_image_iff_exists_fun, Finset.attach, congr, funext, Eq.trans, True, congrFun' and 17 more

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

  6. lemma TwoSidedIdeal.eq_bot_of_map_comap_eq_bot line 94 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Ring, Algebra, IsSimpleRing, Algebra.IsCentral, TwoSidedIdeal, TensorProduct, Eq, TwoSidedIdeal.map, AlgHom, Algebra.TensorProduct.includeRight, OrderHom, TwoSidedIdeal.comap, MonoidHom.id, Bot.bot

    Proof uses: Sigma, Module.Basis, Nonempty, Module.Free.exists_basis, Finset, Membership.mem, Finset.sum, TensorProduct.tmul, OfNat.ofNat, Finset.induction_on, Classical.propDecidable, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, forall_congr, False, implies_congr, Eq.refl, implies_true and 132 more

    226 instances, coercions and auxiliary constants left out.

    Tactic trace: 75 steps

    Open to load the checked before-and-after goal states.

  7. lemma TensorProduct.map_comap_eq line 180 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Ring, Algebra, IsSimpleRing, Algebra.IsCentral, TwoSidedIdeal, TensorProduct, Eq, TwoSidedIdeal.map, AlgHom, Algebra.TensorProduct.includeRight, OrderHom, TwoSidedIdeal.comap, MonoidHom.id

    Proof uses: Eq.symm, le_antisymm, Bot.bot, Ne, Or, LE.le, eq_or_ne, bot_le, Eq.mpr, TwoSidedIdeal.span, Set.image, id, congrArg, TwoSidedIdeal.map.eq_1, Top.top, Or.resolve_left, IsSimpleOrder.eq_bot_or_eq_top, TwoSidedIdeal.eq_bot_of_map_comap_eq_bot, TwoSidedIdeal.map_bot, Eq.refl and 29 more

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

    Open to load the checked before-and-after goal states.

  8. instance TensorProduct.simple line 205 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Ring, IsSimpleRing, Algebra, Algebra.IsCentral, TensorProduct

    Proof uses: AlgHom, Algebra.TensorProduct.includeRight, IsSimpleRing.mk, IsSimpleOrder.mk, TwoSidedIdeal, Eq, OrderHom, TwoSidedIdeal.comap, MonoidHom.id, Bot.bot, Top.top, Or, IsSimpleOrder.eq_bot_or_eq_top, Or.inl, Eq.mpr, TwoSidedIdeal.map, id, congrArg, Eq.symm, TensorProduct.map_comap_eq and 28 more

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

    Open to load the checked before-and-after goal states.