FLT/Mathlib/RingTheory/TensorProduct/Basis.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

API for base change of free modules

We (presumably) have all this in mathlib for base change on the other side; this is all about: if A is a free R-algebra then A ⊗[R] B is a free B-algebra.

This can probably all be moved into FLT.Hacks.RightActionInstances? The entire file has open scoped TensorProduct.RightActions`.

Imports (10)
Imported by 2 files
  1. def Module.Basis.rightBaseChange line 44 source

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

    Statement uses: CommSemiring, Algebra, Fintype, DecidableEq, Module.Basis, TensorProduct, TensorProduct.RightActions.instModule_fLT

    Proof uses: Module.Basis.ofRepr, LinearEquiv, RingHom.id, TensorProduct.RightActions.instAlgebra_fLT, TensorProduct.RightActions.Algebra.TensorProduct.comm, LinearEquiv.trans, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.refl, Module.Basis.equivFun, TensorProduct.piScalarRight, Finsupp, Finsupp.linearEquivFunOnFinite, LinearEquiv.symm

    27 instances, coercions and auxiliary constants left out.

  2. lemma Module.Basis.rightBaseChange_repr line 58 source

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

    Statement uses: CommSemiring, Algebra, Fintype, DecidableEq, Module.Basis, Eq, Finsupp, LinearEquiv, RingHom.id, TensorProduct, TensorProduct.RightActions.instModule_fLT, Module.Basis.repr, Module.Basis.rightBaseChange, TensorProduct.tmul, Finsupp.single

    Proof uses: Finset.sum, Finset.univ, HSMul.hSMul, Pi.single, OfNat.ofNat, Eq.mpr, id, Eq.rec, Eq.refl, funext, Eq.trans, congrArg, Pi.single_comm, Pi.single_apply_smul, of_eq_true, True, congrFun', ite, Membership.mem, Finset and 21 more

    74 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  3. lemma Module.Basis.rightBaseChange_apply line 71 source

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

    Statement uses: CommSemiring, Algebra, Fintype, DecidableEq, Module.Basis, Eq, TensorProduct, TensorProduct.RightActions.instModule_fLT, Module.Basis.rightBaseChange, TensorProduct.tmul, OfNat.ofNat

    Proof uses: Eq.mpr, Finsupp, LinearEquiv, RingHom.id, Module.Basis.repr, Finsupp.single, id, congrArg, propext, Module.Basis.apply_eq_iff, Module.Basis.rightBaseChange_repr

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. lemma TensorProduct.finrank_rightAlgebra line 87 source

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

    Statement uses: CommRing, CommSemiring, Algebra, Nontrivial, Module.Finite, Module.Free, Eq, Nat, Module.finrank, TensorProduct, TensorProduct.RightActions.instModule_fLT

    Proof uses: RingHom.domain_nontrivial, Algebra.algebraMap, Module.Basis, Module.Free.ChooseBasisIndex, Module.Free.chooseBasis, Module.Basis.rightBaseChange, Eq.mpr, Fintype.card, id, congrArg, Module.finrank_eq_card_basis, Eq.refl

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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