GeometricallyReduced_isReduced_tensorProduct_of_separable.lean`

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib

class IsSeparablyGenerated line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
4 instances, coercions and auxiliary constants left out.
Also declared: APNOutputs/StacksProject/GeometricallyReduced_isGeometricallyReduced_iff_of_separable_algebraic.lean:40 (same declaration text), APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separablyGenerated.lean:40 (same declaration text), APNOutputs/StacksProject/Separability_exists_isPurelyInseparable_isSeparablyGenerated_of_essFiniteType.lean:40 (same declaration text).
class IsSeparableExtensionSP line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
4 instances, coercions and auxiliary constants left out.
Also declared: APNOutputs/StacksProject/GeometricallyReduced_isGeometricallyReduced_iff_of_separable_algebraic.lean:44 (same declaration text), APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separablyGenerated.lean:44 (same declaration text).
class IsSeparablyFinitelyGenerated line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
4 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: APNOutputs/StacksProject/GeometricallyReduced_isGeometricallyReduced_iff_of_separable_algebraic.lean:47 (same statement text; different proof or body), APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separablyGenerated.lean:47 (same statement text; different proof or body). Qualify references as IsSeparablyFinitelyGenerated@path.
lemma isReduced_tensorProduct_symm_helper line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, IsReduced, TensorProduct
Proof uses: AlgEquiv, Algebra.TensorProduct.comm, Function.Injective, AlgEquiv.injective, isReduced_of_injective
44 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma isReduced_mvPolynomial_tensor line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, TensorProduct, MvPolynomial
Proof uses: AlgEquiv, MvPolynomial.scalarRTensorAlgEquiv, Classical.typeDecidableEq, Function.Injective, AlgEquiv.injective, inferInstance, isReduced_of_injective
70 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma helper_isReduced_of_isLocalization line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Submonoid, IsLocalization, IsReduced
Proof uses: IsReduced.mk, IsNilpotent, helper_isReduced_of_isLocalization.match_1, Eq, OfNat.ofNat, Nat, HPow.hPow, Exists.elim, Prod, Subtype, Membership.mem, IsLocalization.mk'_surjective.match_1, IsLocalization.mk', IsLocalization.mk'_surjective, Eq.rec, by_contradiction, Not, absurd, False, Eq.mpr and 47 more
55 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma helper_tensor_isLocalization line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, IsFractionRing, IsLocalization, TensorProduct, Submonoid.map, MonoidHom, AlgHom.toRingHom, Algebra.TensorProduct.includeLeft, nonZeroDivisors, RingHom.toAlgebra, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id
Proof uses: by_contradiction, Not, IsLocalization'.mk, Submonoid.IsLocalizationMap.mk, RingHom, algebraMap, Eq.mpr, Subtype, Membership.mem, Submonoid, IsUnit, TensorProduct.tmul, OfNat.ofNat, id, Eq, Eq.trans, AlgHom, Subtype.mk, forall_congr, And and 70 more
187 instances, coercions and auxiliary constants left out.
Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_of_algebra_adjoin_transcendental line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Set, IsTranscendenceBasis, Membership.mem, IsReduced, TensorProduct, Subtype, Subalgebra, Algebra.adjoin
Proof uses: AlgebraicIndependent, And.left, AlgebraicIndepOn, id, HasSubset.Subset, Set.range, Eq, AlgEquiv, MvPolynomial, AlgebraicIndependent.aevalEquiv, Subtype.range_val, AlgEquiv.trans, Subalgebra.equivOfEq, Eq.mpr, congrArg, Eq.refl, Algebra.TensorProduct.congr, AlgEquiv.refl, isReduced_mvPolynomial_tensor, isReduced_of_injective and 2 more
98 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma helper_isFractionRing line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, Subalgebra, Algebra.adjoin, IntermediateField, IntermediateField.adjoin, IsFractionRing, Subtype, Membership.mem, RingHom.toAlgebra, IntermediateField.toSubalgebra, AlgHom.toRingHom, Subalgebra.inclusion, IntermediateField.algebra_adjoin_le_adjoin
Proof uses: IsLocalization'.mk, nonZeroDivisors, Submonoid.IsLocalizationMap.mk, RingHom, algebraMap, Submonoid, Ne.isUnit, Function.comp, Eq, OfNat.ofNat, False, nonZeroDivisors.ne_zero, Subtype.property, Subtype.eq, congr_arg, Eq.mpr, Exists, Prod, HMul.hMul, Prod.snd and 45 more
121 instances, coercions and auxiliary constants left out.
Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_of_transcendence_basis line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Set, IsTranscendenceBasis, Membership.mem, IsReduced, TensorProduct, Subtype, IntermediateField, IntermediateField.adjoin
Proof uses: Subalgebra, Algebra.adjoin, LE.le, IntermediateField.toSubalgebra, IntermediateField.algebra_adjoin_le_adjoin, isReduced_tensorProduct_of_algebra_adjoin_transcendental, IsLocalization, Submonoid.map, MonoidHom, AlgHom.toRingHom, Algebra.TensorProduct.includeLeft, nonZeroDivisors, RingHom.toAlgebra, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, Subalgebra.inclusion, IsScalarTower.of_algebraMap_eq, rfl, RingHom, algebraMap and 4 more
121 instances, coercions and auxiliary constants left out.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_of_separable_algebraic_iso line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Nonempty, AlgEquiv, TensorProduct
Proof uses: Algebra.TensorProduct.assoc, Algebra.TensorProduct.rid, Algebra.TensorProduct.congr, AlgEquiv.restrictScalars, AlgEquiv.refl, AlgEquiv.trans, AlgEquiv.symm, Nonempty.intro
78 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma exists_intermediateField_fg_over_F line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Subalgebra, Subalgebra.FG, Exists, IntermediateField, And, LE.le, IntermediateField.toSubalgebra, IntermediateField.FG
Proof uses: Finset, Eq, Algebra.adjoin, Exists.intro, IntermediateField.adjoin, And.intro, Eq.mpr, id, congrArg, Eq.symm, IntermediateField.algebra_adjoin_le_adjoin, IntermediateField.fg_adjoin_finset
21 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma helper_tensor_map_injective_over_F line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Subalgebra, IntermediateField, LE.le, IntermediateField.toSubalgebra, Function.Injective, TensorProduct, Subtype, Membership.mem, AlgHom, Algebra.TensorProduct.map, AlgHom.id, Subalgebra.inclusion
Proof uses: Module.Flat.lTensor_preserves_injective_linearMap, AlgHom.toLinearMap, Subalgebra.inclusion_injective
81 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isReduced_iff_sq_eq_zero line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Iff, IsReduced, Eq, HPow.hPow, Nat, OfNat.ofNat
Proof uses: isReduced_iff_pow_one_lt, Nat.le.refl, Nat.succ
18 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma helper_module_free line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, CommRing, IsReduced, FiniteDimensional, Module.Free, TensorProduct
Proof uses: inferInstance
73 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma helper_module_finite line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, CommRing, IsReduced, FiniteDimensional, Module.Finite, TensorProduct
Proof uses: inferInstance
59 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_of_finite_separable_trace line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, CommRing, IsReduced, FiniteDimensional, Module.Free, TensorProduct, Module.Finite, Eq, HPow.hPow, Nat, OfNat.ofNat, LinearMap, RingHom.id, Algebra.trace
Proof uses: IsNilpotent, Module.End, AlgHom, Algebra.lmul, Exists.intro, LinearMap.ext, Trans.trans, HMul.hMul, rfl, Eq.symm, mul_assoc, Eq.mpr, id, congrArg, sq, Eq.refl, MulZeroClass.zero_mul, LinearMap.trace, LinearMap.isNilpotent_trace_of_isNilpotent, IsReduced.eq_zero
114 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma helper_lmul_tensor line 204 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, Eq, Module.End, TensorProduct, AlgHom, Algebra.lmul, TensorProduct.tmul, HSMul.hSMul, LinearMap, RingHom.id, LinearMap.baseChange
Proof uses: Eq.mpr, HMul.hMul, LinearMap.mul, id, TensorProduct.induction_on, of_eq_true, OfNat.ofNat, Eq.trans, True, congr, congrArg, MulZeroClass.mul_zero, map_zero, RingHom, smul_zero, eq_self, HAdd.hAdd, mul_add, map_add, smul_add
128 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma helper_trace_tensor line 209 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, FiniteDimensional, Module.Free, TensorProduct, Module.Finite, Eq, LinearMap, RingHom.id, Algebra.trace, TensorProduct.tmul, HMul.hMul, RingHom, algebraMap
Proof uses: LinearMap.trace, AlgHom, Module.End, Algebra.lmul, rfl, Eq.mpr, id, congrArg, HSMul.hSMul, LinearMap.baseChange, helper_lmul_tensor, LinearMap.map_smul, LinearMap.trace_baseChange, Eq.refl
110 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma helper_z_eq_sum line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, TensorProduct, Fintype, DecidableEq, Module.Basis, Exists, Eq, Finset.sum, Finset.univ, TensorProduct.tmul
Proof uses: TensorProduct.induction_on, Exists.intro, OfNat.ofNat, of_eq_true, Eq.trans, True, congrArg, Fintype.elems, Finset.sum_congr, Eq.refl, Finset, Membership.mem, TensorProduct.zero_tmul, Finset.sum_const_zero, eq_self, Eq.rec, HSMul.hSMul, Finsupp, LinearEquiv, RingHom.id and 13 more
85 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma helper_exists_dual_basis line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, FiniteDimensional, Fintype, DecidableEq, Module.Basis, Exists, Eq, LinearMap, RingHom.id, Algebra.trace, HMul.hMul, ite, OfNat.ofNat
Proof uses: LinearMap.BilinForm.Nondegenerate, Algebra.traceForm, traceForm_nondegenerate, LinearMap.BilinForm.dualBasis, Exists.intro, Eq.mpr, id, congrArg, mul_comm, Eq.refl, LinearMap.BilinForm, rfl, LinearMap.BilinForm.apply_dualBasis_left
80 instances, coercions and auxiliary constants left out.
Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma helper_trace_sum line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, FiniteDimensional, Module.Free, TensorProduct, Module.Finite, Fintype, DecidableEq, Eq, LinearMap, RingHom.id, Algebra.trace, HMul.hMul, ite, OfNat.ofNat, Finset.sum, Finset.univ, TensorProduct.tmul
Proof uses: Eq.mpr, id, congrArg, Finset.sum_mul, Finset.sum_congr, rfl, Finset, Membership.mem, Algebra.TensorProduct.tmul_mul_tmul, mul_one, Eq.refl, map_sum, RingHom, algebraMap, helper_trace_tensor, dite, congr, if_pos, of_eq_true, Eq.trans and 14 more
111 instances, coercions and auxiliary constants left out.
Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma helper_trace_zero_implies_zero line 271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, CommRing, IsReduced, FiniteDimensional, Module.Free, TensorProduct, Module.Finite, Eq, LinearMap, RingHom.id, Algebra.trace, HMul.hMul, OfNat.ofNat
Proof uses: Module.Free.ChooseBasisIndex, Module.Basis, Module.Free.chooseBasis, Exists, Finset.sum, Finset.univ, TensorProduct.tmul, helper_z_eq_sum, Classical.typeDecidableEq, ite, helper_exists_dual_basis, helper_trace_sum, Eq.symm, Eq.mp, congrArg, Eq.mpr, id, TensorProduct.zero_tmul, Eq.refl, Finset.sum_eq_zero and 2 more
110 instances, coercions and auxiliary constants left out.
Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_of_finite_separable_field line 296 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, FiniteDimensional, Algebra.IsSeparable, CommRing, IsReduced, TensorProduct
Proof uses: Eq.mpr, Eq, HPow.hPow, Nat, OfNat.ofNat, id, congrArg, propext, isReduced_iff_sq_eq_zero, LinearMap, RingHom.id, Algebra.trace, HMul.hMul, Trans.trans, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.mul_congr and 22 more
81 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma helper_fin_dim_of_fg_algebraic line 312 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsAlgebraic, IntermediateField, IntermediateField.FG, FiniteDimensional, Subtype, Membership.mem
Proof uses: Finset, Eq, IntermediateField.adjoin, IntermediateField.finiteDimensional_adjoin, Set, Algebra.IsIntegral.isIntegral
71 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma helper_is_separable_subfield line 317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, IntermediateField, Subtype, Membership.mem
Proof uses: inferInstance
61 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_of_separable_algebraic_helper line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Algebra.IsSeparable, Algebra.IsAlgebraic, IsReduced, TensorProduct
Proof uses: IsReduced.tensorProduct_of_flat_of_forall_fg, Subalgebra, Subalgebra.FG, IntermediateField, And, LE.le, IntermediateField.toSubalgebra, IntermediateField.FG, Exists, Subtype, Membership.mem, exists_intermediateField_fg_over_F, FiniteDimensional, helper_fin_dim_of_fg_algebraic, helper_is_separable_subfield, isReduced_tensorProduct_of_finite_separable_field, Function.Injective, AlgHom, Algebra.TensorProduct.map, AlgHom.id and 3 more
113 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_of_separable_algebraic line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Algebra.IsSeparable, Algebra.IsAlgebraic, IsReduced, TensorProduct
Proof uses: isReduced_tensorProduct_of_separable_algebraic.match_1, Nonempty, AlgEquiv, isReduced_tensorProduct_of_separable_algebraic_iso, isReduced_tensorProduct_of_separable_algebraic_helper, isReduced_tensorProduct_symm_helper, isReduced_of_injective, AlgEquiv.injective
70 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_of_separably_generated line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsSeparablyGenerated, IsReduced, TensorProduct
Proof uses: isReduced_tensorProduct_of_separably_generated.match_1, Exists, Set, And, IsTranscendenceBasis, Membership.mem, Algebra.IsSeparable, Subtype, IntermediateField, IntermediateField.adjoin, IsSeparablyGenerated.out, isReduced_tensorProduct_of_transcendence_basis, isReduced_tensorProduct_of_separable_algebraic
81 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma helper_ess_finite line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Finset, Algebra.EssFiniteType, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin
Proof uses: Iff.mpr, IntermediateField.FG, IntermediateField.essFiniteType_iff, IntermediateField.fg_adjoin_finset
60 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma helper_subalgebra_le line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Subalgebra, Finset, Eq, Algebra.adjoin, LE.le, IntermediateField.toSubalgebra, IntermediateField.adjoin
Proof uses: Eq.rec, IntermediateField.algebra_adjoin_le_adjoin
22 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma helper_map_injective line 361 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Subalgebra, IntermediateField, LE.le, IntermediateField.toSubalgebra, Function.Injective, TensorProduct, Subtype, Membership.mem, AlgHom, Algebra.TensorProduct.map, AlgHom.id, Subalgebra.inclusion
Proof uses: Module.Flat.lTensor_preserves_injective_linearMap, AlgHom.toLinearMap, Subalgebra.inclusion_injective
81 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma helper_is_reduced line 366 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsSeparableExtensionSP, IsReduced, TensorProduct
Proof uses: isReduced_tensorProduct_symm_helper, IsReduced.tensorProduct_of_flat_of_forall_fg, Subalgebra, Subalgebra.FG, Finset, Eq, Algebra.adjoin, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, Algebra.EssFiniteType, helper_ess_finite, IsSeparablyGenerated, IsSeparableExtensionSP.out, isReduced_tensorProduct_of_separably_generated, LE.le, IntermediateField.toSubalgebra, helper_subalgebra_le, Function.Injective and 6 more
104 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem isReduced_tensorProduct_of_separable line 383 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsSeparableExtensionSP, IsReduced, TensorProduct
Proof uses: helper_is_reduced
41 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.