AlgebrasOverFields_geometrically_irreducible_tfae.lean`

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib

class GeometricallyIrreducibleAlgebra line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra
4 instances, coercions and auxiliary constants left out.
Also declared: APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_of_directed_colimit.lean:41 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_transitive.lean:41 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_minimalPrimes_bijection_of_geometrically_IrreducibleAlgebra.lean:41 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean:41 (same declaration text).
def alg_dir_lim line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Preorder, IsDirected, LE.le, Nonempty, CommRing, Algebra, AlgHom, Ring.DirectLimit
Proof uses: Classical.arbitrary, RingHom, Ring.DirectLimit.of, RingHom.toAlgebra, RingHom.comp, algebraMap
17 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_of_directed_colimit.lean:46 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_transitive.lean:46 (same statement text; different proof or body), APNOutputs/StacksProject/AlgebrasOverFields_minimalPrimes_bijection_of_geometrically_IrreducibleAlgebra.lean:46 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean:46 (same declaration text). Qualify references as alg_dir_lim@path.
lemma irreducibleSpace_of_surjective_continuous line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Function.Surjective, Continuous, IrreducibleSpace
Proof uses: Eq.mpr, IsIrreducible, Top.top, Set, id, Eq, Eq.rec, Set.image, Set.preimage, IsIrreducible.image, Eq.mp, Continuous.continuousOn, Function.Surjective.image_preimage
3 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma test_nilradical_prime line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Iff, IrreducibleSpace, PrimeSpectrum, Ideal.IsPrime, nilradical
Proof uses: Iff.intro, Eq.mpr, InfSet.sInf, Ideal, setOf, id, Eq, congrArg, nilradical_eq_sInf, And, Ne, Top.top, Membership.mem, HMul.hMul, Or, Eq.trans, funext, Set, forall_congr, implies_congr and 70 more
62 instances, coercions and auxiliary constants left out.
Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma test_integral_surj line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, RingHom.IsIntegral, Function.Injective, Function.Surjective, PrimeSpectrum, PrimeSpectrum.comap
Proof uses: RingHom.IsIntegral.comap_surjective
12 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma isIntegral_tmul_one line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, RingHom, TensorProduct, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, IsIntegral, RingHom.toAlgebra, TensorProduct.tmul, OfNat.ofNat
Proof uses: Exists.intro, Polynomial, And, Polynomial.Monic, Eq, Polynomial.eval₂, algebraMap, HSub.hSub, Polynomial.X, Polynomial.C, And.intro, Polynomial.monic_X_sub_C, of_eq_true, AlgHom, Eq.trans, True, congrArg, Polynomial.eval₂_sub, congr, Polynomial.eval₂_X and 6 more
109 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma isIntegral_one_tmul line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, IsIntegral, RingHom, TensorProduct, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, RingHom.toAlgebra, TensorProduct.tmul, OfNat.ofNat
Proof uses: Polynomial, And, Polynomial.Monic, Eq, Polynomial.eval₂, algebraMap, id, Exists.intro, AlgHom, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, LinearMap, RingHom.id, Polynomial.monomial, Polynomial.coeff, And.intro, Polynomial.monic_of_degree_le and 60 more
160 instances, coercions and auxiliary constants left out.
Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma tmul_eq_mul line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Eq, TensorProduct, TensorProduct.tmul, HMul.hMul, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrArg, congr, mul_one, one_mul, eq_self
56 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma integral_tensor_extension line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Algebra.IsIntegral, RingHom.IsIntegral, TensorProduct, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom
Proof uses: RingHom, Membership.mem, Subalgebra, RingHom.toAlgebra, integralClosure, TensorProduct.induction_on, Subalgebra.zero_mem, IsIntegral, Algebra.IsIntegral.isIntegral, TensorProduct.tmul, OfNat.ofNat, isIntegral_tmul_one, isIntegral_one_tmul, Eq, HMul.hMul, tmul_eq_mul, Eq.mpr, id, congrArg, Subalgebra.mul_mem and 1 more
81 instances, coercions and auxiliary constants left out.
Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma injective_tensor_extension line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Function.Injective, TensorProduct, RingHom, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom
Proof uses: Module.Flat.lTensor_preserves_injective_linearMap, AlgHom.toLinearMap, RingHom.injective, algebraMap
71 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma irreducible_of_isIntegral_surj line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Algebra.IsIntegral, IrreducibleSpace, PrimeSpectrum, TensorProduct
Proof uses: RingHom.IsIntegral, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, integral_tensor_extension, Function.Injective, RingHom, injective_tensor_extension, Function.Surjective, PrimeSpectrum.comap, test_integral_surj, Continuous, PrimeSpectrum.continuous_comap, irreducibleSpace_of_surjective_continuous
61 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma irreducible_of_algebraic_closed_extension line 162 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsAlgClosed, IrreducibleSpace, PrimeSpectrum, TensorProduct
Proof uses: AlgebraicClosure, inferInstance, Algebra.IsIntegral, irreducible_of_isIntegral_surj
51 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma isPrime_of_power line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Function.Injective, Exists, Nat, And, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.range, HPow.hPow, Ideal.IsPrime, nilradical
Proof uses: Mathlib.Tactic.Contrapose.contrapose₁, Not, Eq.mpr, id, Eq, congrArg, funext, Mathlib.Tactic.Contrapose.contrapose₂, Ne, Ideal, Ideal.radical, Top.top, HMul.hMul, Or, implies_congr, Eq.trans, binderNameHint, forall_congr, Eq.refl, congr and 38 more
87 instances, coercions and auxiliary constants left out.
Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma isPrime_of_images line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Nonempty, Preorder, IsDirected, LE.le, RingHom, Ideal.IsPrime, nilradical, Exists, Eq, Function.Injective, RingHom.comp
Proof uses: Ne, Ideal, Top.top, Membership.mem, OfNat.ofNat, Eq.mpr, id, congrArg, True.intro, Nat, HPow.hPow, False, Ideal.IsPrime.ne_top, Exists.intro, map_one, map_zero, map_pow, one_pow, Eq.symm, Eq.refl and 13 more
62 instances, coercions and auxiliary constants left out.
Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
abbrev FinSepSubext line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
Proof uses: Subtype, IntermediateField, And, Module.Finite, Membership.mem, Algebra.IsSeparable
30 instances, coercions and auxiliary constants left out.
instance (instance at line 262) line 262 source
lemma tfae_2_to_3_directed line 265 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsDirected, FinSepSubext, LE.le, IntermediateField, And, Module.Finite, Subtype, Membership.mem, Algebra.IsSeparable
Proof uses: IsDirected.mk, Classical.byContradiction, Exists, Not, Eq, False, Subtype.mk, And.intro, Eq.mpr, Eq.refl, Exists.elim, Max.max, Eq.mp, Eq.trans, forall_congr, implies_congr_ctx, congrArg, funext, inferInstance, Function.comp and 7 more
79 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
instance (instance at line 277) line 277 source
lemma tfae_2_to_3_nonempty line 280 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Nonempty, FinSepSubext
Proof uses: Nonempty.intro, Subtype.mk, IntermediateField, And, Module.Finite, Subtype, Membership.mem, Algebra.IsSeparable, Bot.bot, And.intro, inferInstance
42 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance (instance at line 285) line 285 source
abbrev tfae_2_to_3_A_i line 288 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, FinSepSubext
Proof uses: TensorProduct, Subtype, Membership.mem, IntermediateField, And, Module.Finite, Algebra.IsSeparable
34 instances, coercions and auxiliary constants left out.
abbrev tfae_2_to_3_f line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, FinSepSubext, RingHom, tfae_2_to_3_A_i, TensorProduct, Subtype, Membership.mem, IntermediateField, And, Module.Finite, Algebra.IsSeparable
Proof uses: AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom
79 instances, coercions and auxiliary constants left out.
lemma tfae_2_to_3_inj line 295 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, FinSepSubext, Function.Injective, tfae_2_to_3_A_i, TensorProduct, RingHom, Subtype, Membership.mem, IntermediateField, And, Module.Finite, Algebra.IsSeparable, tfae_2_to_3_f
Proof uses: id, Module.Flat.lTensor_preserves_injective_linearMap, AlgHom.toLinearMap, IsScalarTower.toAlgHom, Subtype.coe_injective
105 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma tfae_2_to_3_dir line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, FinSepSubext, LE.le, IntermediateField, And, Module.Finite, Subtype, Membership.mem, Algebra.IsSeparable, Exists, RingHom, tfae_2_to_3_A_i, Eq, TensorProduct, RingHom.comp, tfae_2_to_3_f
Proof uses: AlgHom, Subalgebra.inclusion, IntermediateField.toSubalgebra, Exists.intro, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, Eq.mpr, IsScalarTower.toAlgHom, id, Subtype.mk, And.intro, Eq.trans, LinearMap, RingHom.id, TensorProduct.map, AlgHom.toLinearMap, LinearMap.comp, TensorProduct.map_map, Eq.refl and 1 more
117 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma tfae_2_to_3_surj_zero line 308 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsSepClosure, CommRing, Exists, FinSepSubext, tfae_2_to_3_A_i, Eq, TensorProduct, RingHom, Subtype, Membership.mem, IntermediateField, And, Module.Finite, Algebra.IsSeparable, tfae_2_to_3_f, OfNat.ofNat
Proof uses: IsSepClosed, IsSepClosure.mk, Eq.mpr, Subtype.mk, AlgHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, id, Exists.intro, Bot.bot, And.intro, inferInstance, Eq.refl
114 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma tfae_2_to_3_surj_tmul line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsSepClosure, CommRing, Exists, FinSepSubext, tfae_2_to_3_A_i, Eq, TensorProduct, RingHom, Subtype, Membership.mem, IntermediateField, And, Module.Finite, Algebra.IsSeparable, tfae_2_to_3_f, TensorProduct.tmul
Proof uses: Eq.mpr, Subtype.mk, AlgHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, id, IsSepClosed, IsSepClosure.mk, Exists.intro, IntermediateField.adjoin, Singleton.singleton, Set, And.intro, IntermediateField.adjoin.finiteDimensional, Algebra.IsSeparable.isIntegral, inferInstance, IntermediateField.subset_adjoin, rfl, Eq.refl
101 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma tfae_2_to_3_surj_add line 322 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsSepClosure, CommRing, TensorProduct, Exists, FinSepSubext, tfae_2_to_3_A_i, Eq, RingHom, Subtype, Membership.mem, IntermediateField, And, Module.Finite, Algebra.IsSeparable, tfae_2_to_3_f, HAdd.hAdd
Proof uses: LE.le, directed_of, tfae_2_to_3_directed, RingHom.comp, tfae_2_to_3_dir, Exists.intro, Trans.trans, rfl, Eq.mpr, id, congrArg, Eq.refl, RingHom.map_add
102 instances, coercions and auxiliary constants left out.
Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma tfae_2_to_3_surj line 345 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsSepClosure, CommRing, TensorProduct, Exists, FinSepSubext, tfae_2_to_3_A_i, Eq, RingHom, Subtype, Membership.mem, IntermediateField, And, Module.Finite, Algebra.IsSeparable, tfae_2_to_3_f
Proof uses: TensorProduct.induction_on, tfae_2_to_3_surj_zero, tfae_2_to_3_surj_tmul, tfae_2_to_3_surj_add
86 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma tfae_2_to_3 line 352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Module.Finite, Algebra.IsSeparable, IrreducibleSpace, PrimeSpectrum, TensorProduct, IsSepClosure
Proof uses: FinSepSubext, Ideal.IsPrime, tfae_2_to_3_A_i, Subtype, Membership.mem, IntermediateField, And, nilradical, And.left, Subtype.property, And.right, Iff.mp, test_nilradical_prime, Exists, Eq, RingHom, tfae_2_to_3_f, tfae_2_to_3_surj, Function.Injective, tfae_2_to_3_inj and 6 more
80 instances, coercions and auxiliary constants left out.
Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma test_is_sep_closure line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsAlgClosed, IsSepClosure, Subtype, Membership.mem, IntermediateField, separableClosure
Proof uses: inferInstance
60 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma purely_insep_exists_pow_zero line 378 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsAlgebraic, CharZero, IsSeparable
Proof uses: Irreducible.separable, minpoly, minpoly.irreducible, Algebra.IsIntegral.isIntegral
24 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma purely_insep_pow_add_expChar line 382 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, TensorProduct, Nat, ExpChar, Eq, HPow.hPow, HAdd.hAdd
Proof uses: HEq, CharZero, OfNat.ofNat, ExpChar.zero, of_eq_true, Eq.trans, True, congr, congrArg, one_pow, pow_one, eq_self, eq_true, True.intro, Eq.symm, Nat.Prime, CharP, ExpChar.prime, Exists, CharP.exists and 27 more
91 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma test_is_purely_insep line 396 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsAlgebraic, IsPurelyInseparable, Subtype, Membership.mem, IntermediateField, separableClosure
Proof uses: inferInstance
29 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma purely_insep_exists_pow_expChar line 400 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsAlgebraic, Nat, ExpChar, Exists, Membership.mem, IntermediateField, separableClosure, HPow.hPow
Proof uses: IsPurelyInseparable, Subtype, test_is_purely_insep, Exists.intro, Exists.choose, Subring, RingHom.range, algebraMap, Eq.mp, Ring, IsDomain, propext, isPurelyInseparable_iff_pow_mem, Exists.elim, Eq, RingHom, Exists.choose_spec, Eq.subst, Subtype.property
45 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma tfae_3_to_4_pow_zero line 406 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsAlgebraic, Nat, ExpChar, IntermediateField, separableClosure, RingHom, TensorProduct, Subtype, Membership.mem, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, Exists, Set, Set.range, HPow.hPow and 1 more
Proof uses: Exists.intro, Eq, Eq.mpr, id, congrArg, pow_zero, pow_one, Eq.refl, map_zero
120 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma tfae_3_to_4_pow_tmul line 417 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsAlgebraic, Nat, ExpChar, IntermediateField, separableClosure, RingHom, TensorProduct, Subtype, Membership.mem, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, Exists, Set, Set.range, HPow.hPow and 1 more
Proof uses: purely_insep_exists_pow_expChar, Exists.intro, Eq, Subtype.mk, of_eq_true, Eq.trans, True, congrArg, Algebra.TensorProduct.tmul_pow, eq_self, eq_true, True.intro
101 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma tfae_3_to_4_pow_add line 428 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsAlgebraic, TensorProduct, Nat, ExpChar, IntermediateField, separableClosure, RingHom, Subtype, Membership.mem, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, Exists, Set, Set.range, HPow.hPow and 1 more
Proof uses: Eq.mpr, Eq, id, congrArg, funext, Exists.elim, Eq.mp, tfae_3_to_4_pow_add.match_1, Exists.intro, Max.max, HEq, CharZero, OfNat.ofNat, ExpChar.zero, of_eq_true, AlgHom, Eq.trans, True, congr, map_add and 43 more
169 instances, coercions and auxiliary constants left out.
Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma tfae_3_to_4_pow_expChar line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsAlgebraic, Nat, ExpChar, IntermediateField, separableClosure, RingHom, TensorProduct, Subtype, Membership.mem, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, Exists, Set, Set.range, HPow.hPow
Proof uses: TensorProduct.induction_on, tfae_3_to_4_pow_zero, tfae_3_to_4_pow_tmul, tfae_3_to_4_pow_add
100 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma tfae_3_to_4_pow line 467 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsAlgebraic, IntermediateField, separableClosure, RingHom, TensorProduct, Subtype, Membership.mem, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, Exists, Nat, And, LT.lt, OfNat.ofNat, Set and 2 more
Proof uses: ringExpChar, tfae_3_to_4_pow_expChar, Exists.intro, And.intro, ExpChar, expChar_pos, pow_pos
110 instances, coercions and auxiliary constants left out.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ideal_map_nilpotent line 481 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Ideal, Membership.mem, IsNilpotent, Ideal.map
Proof uses: Finset, And, HasSubset.Subset, Set, Exists, Subtype, Eq, Finset.sum, Finset.univ, HSMul.hSMul, Iff.mp, Submodule, Submodule.span, Set.image, Submodule.mem_span_image_iff_exists_fun, Exists.intro, And.elim, ideal_map_nilpotent.match_1, Eq.rec, isNilpotent_sum and 5 more
57 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ker_quotient_tensor line 487 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Eq, TensorProduct, RingHom.ker, HasQuotient.Quotient, RingHom, AlgHom.toRingHom, Algebra.TensorProduct.map, Ideal.Quotient.mkₐ, AlgHom.id, Ideal.map, Algebra.TensorProduct.includeLeft
Proof uses: AlgHom, le_antisymm, Membership.mem, Submodule, Ideal.Quotient.liftₐ, AlgHom.comp, Iff.mpr, Ideal.Quotient.mk, OfNat.ofNat, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_map_of_mem, Algebra.TensorProduct.includeRight, HMul.hMul, mul_comm, Algebra.TensorProduct.lift, Algebra.TensorProduct.ext, AlgHom.ext, id, TensorProduct.tmul, Eq.mpr and 19 more
142 instances, coercions and auxiliary constants left out.
Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
lemma tensorProduct_injective_of_field line 536 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AlgHom, Function.Injective, TensorProduct, Algebra.TensorProduct.map, AlgHom.id
Proof uses: Module.Flat.rTensor_preserves_injective_linearMap, AlgHom.toLinearMap
64 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma isSepClosure_self line 543 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, IsAlgClosed, IsSepClosure
Proof uses: IsSepClosure.mk, inferInstance, IsSepClosed, Algebra.IsSeparable
13 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma quotient_max_ideal_equiv_K line 548 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, IsAlgClosed, CommRing, Algebra, Algebra.FiniteType, Ideal, Ideal.IsMaximal, Nonempty, AlgEquiv, HasQuotient.Quotient
Proof uses: Iff, IsField, Ideal.Quotient.maximal_ideal_iff_isField_quotient, IsField.toField, Iff.mp, Nonempty.intro, AlgEquiv.symm, AlgEquiv.ofBijective, Algebra.ofId, And.intro, Function.Injective, AlgHom, Function.Surjective, RingHom.injective, AlgHom.toRingHom, Eq, WithBot, Nat, Polynomial.degree, minpoly and 10 more
63 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ideal_jacobson_bot_of_finiteType_field line 556 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, IsAlgClosed, CommRing, IsDomain, Algebra, Algebra.FiniteType, Eq, Ideal, Ideal.jacobson, Bot.bot
Proof uses: IsJacobsonRing, isJacobsonRing_of_finiteType, Ideal.IsRadical, Ideal.isRadical_bot
42 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma quotient_tensor_domain line 562 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, IsAlgClosed, CommRing, Algebra, Algebra.FiniteType, Ideal, Ideal.IsMaximal, IsDomain, TensorProduct, HasQuotient.Quotient
Proof uses: quotient_tensor_domain.match_1, Nonempty, AlgEquiv, quotient_max_ideal_equiv_K, Algebra.TensorProduct.congr, AlgEquiv.refl, Algebra.TensorProduct.lid, RingEquiv, AlgEquiv.toRingEquiv, AlgEquiv.trans, IsDomain.mk, NoZeroDivisors.mk, Eq, HMul.hMul, OfNat.ofNat, Eq.mpr, id, congrArg, Eq.refl, Or and 17 more
115 instances, coercions and auxiliary constants left out.
Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma ideal_prod_zero_of_max line 587 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDomain, Eq, Ideal, Ideal.jacobson, Bot.bot, Finset, Ideal.IsMaximal, Or, Membership.mem, OfNat.ofNat
Proof uses: Iff.mpr, Not, Classical.or_iff_not_imp_left, by_contra, Function.comp, False, Or.resolve_right, Set, setOf, And, LE.le, HMul.hMul, Iff.mp, mul_eq_zero, Eq.mp, Iff, InfSet.sInf, forall_congr, congrArg, And.right and 7 more
54 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma tensor_eq_sum_finite line 595 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, TensorProduct, Exists, Finset, Eq, Finset.sum, TensorProduct.tmul
Proof uses: TensorProduct.induction_on, Exists.intro, OfNat.ofNat, EmptyCollection.emptyCollection, rfl, Singleton.singleton, of_eq_true, Eq.trans, True, congrArg, Finset.sum_congr, Eq.refl, Membership.mem, Finset.sum_singleton, eq_self, tensor_eq_sum_finite.match_1, HAdd.hAdd, Union.union, Classical.propDecidable, ite and 14 more
63 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma test_basis_again line 604 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Finset, Exists, And, HasSubset.Subset, LinearIndependent, Subtype, Membership.mem, Eq, Submodule, Submodule.span
Proof uses: Exists.elim, Set, Finset.toSet, exists_linearIndependent, Exists.imp, And.intro, Set.Finite.exists_finset_coe, Set.Finite.subset, Finset.finite_toSet, And.left
49 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma tensor_eq_sum_indep_of_span line 609 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Finset, LE.le, Submodule, Submodule.span, Exists, Eq, TensorProduct, Finset.sum, TensorProduct.tmul
Proof uses: Membership.mem, Exists.elim, And, HasSubset.Subset, Set, Function.support, HSMul.hSMul, Iff.mp, Submodule.mem_span_finset, Eq.mp, Exists.intro, Eq.trans, Eq.rec, TensorProduct.tmul_sum, And.right, Finset.sum_congr, rfl, Eq.symm, TensorProduct.smul_tmul, Finset.sum_comm and 9 more
84 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma tensor_eq_sum_indep line 618 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, TensorProduct, Exists, Finset, And, LinearIndependent, Subtype, Membership.mem, Eq, Finset.sum, TensorProduct.tmul
Proof uses: tensor_eq_sum_finite, HasSubset.Subset, Submodule, Submodule.span, test_basis_again, LE.le, Eq.mpr, id, congrArg, le_refl, tensor_eq_sum_indep_of_span, Exists.intro, And.intro, Eq.refl
55 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma sum_tensor_in_ker_iff line 630 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, IsAlgClosed, CommRing, Algebra, Algebra.FiniteType, Ideal, Ideal.IsMaximal, Finset, LinearIndependent, Subtype, Membership.mem, Iff, Eq, TensorProduct, HasQuotient.Quotient, RingHom, AlgHom.toRingHom, Algebra.TensorProduct.map, Ideal.Quotient.mkₐ, AlgHom.id and 3 more
Proof uses: Eq.mpr, Finset.attach, Ideal.Quotient.mk, id, congr, AlgHom, congrArg, Eq.trans, AddCommMonoid, Eq.symm, Finset.sum_attach, map_sum, Finset.sum_congr, Eq.refl, forall_congr, implies_congr, Module.Basis, Module.Free.ChooseBasisIndex, Module.Free.chooseBasis, Prod and 42 more
169 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma sum_tensor_eq_zero_of_coeff_zero line 642 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Finset, Membership.mem, Eq, OfNat.ofNat, TensorProduct, Finset.sum, TensorProduct.tmul
Proof uses: Eq.mpr, id, congrArg, TensorProduct.zero_tmul, Eq.refl, Finset.sum_eq_zero
54 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma isDomain_tensorProduct_of_fg_domain line 650 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, IsAlgClosed, CommRing, IsDomain, Algebra, Algebra.FiniteType, TensorProduct
Proof uses: IsDomain.mk, NoZeroDivisors.mk, Eq, HMul.hMul, OfNat.ofNat, Finset, Exists, And, LinearIndependent, Subtype, Membership.mem, Finset.sum, TensorProduct.tmul, Or, tensor_eq_sum_indep, Ideal, Ideal.IsMaximal, RingHom, HasQuotient.Quotient, AlgHom.toRingHom and 23 more
106 instances, coercions and auxiliary constants left out.
Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
def InSubalgebra line 693 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Subalgebra, TensorProduct
Proof uses: Membership.mem, Submodule, LinearMap.range, Subtype, RingHom.id, AlgHom.toLinearMap, Algebra.TensorProduct.map, Subalgebra.val, AlgHom.id
46 instances, coercions and auxiliary constants left out.
lemma inSubalgebra_mono line 696 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Subalgebra, LE.le, TensorProduct, InSubalgebra
Proof uses: Subtype, Membership.mem, Eq, LinearMap, RingHom.id, AlgHom.toLinearMap, Algebra.TensorProduct.map, Subalgebra.val, AlgHom.id, Exists.intro, AlgHom, Subalgebra.inclusion, Eq.mpr, id, congrArg, Eq.symm, AlgHom.comp, Algebra.TensorProduct.ext, AlgHom.ext, Algebra.TensorProduct.includeLeft and 5 more
75 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma isDomain_of_subalgebra line 711 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Subalgebra, IsDomain, Subtype, Membership.mem
18 instances, coercions and auxiliary constants left out.
lemma exists_subalgebra_of_tensor line 715 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, TensorProduct, Exists, Finset, InSubalgebra, Algebra.adjoin
Proof uses: TensorProduct.induction_on, Exists.intro, OfNat.ofNat, EmptyCollection.emptyCollection, Subtype, Membership.mem, Subalgebra, Eq, LinearMap, RingHom.id, AlgHom.toLinearMap, Algebra.TensorProduct.map, Subalgebra.val, AlgHom.id, map_zero, RingHom, TensorProduct.tmul, Singleton.singleton, Algebra.subset_adjoin, of_eq_true and 20 more
80 instances, coercions and auxiliary constants left out.
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma finiteType_adjoin_finset line 744 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Finset, Algebra.FiniteType, Subtype, Membership.mem, Subalgebra, Algebra.adjoin
Proof uses: Algebra.FiniteType.mk, Exists.intro, Eq, Top.top, Finset.preimage, Function.Injective.injOn, Subtype.coe_injective, Set.preimage, of_eq_true, Eq.trans, True, congrArg, Set, Finset.coe_preimage, Algebra.adjoin_adjoin_coe_preimage, eq_self, eq_true, True.intro
30 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma isDomain_tensorProduct_of_isAlgClosed_field line 748 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsAlgClosed, IsDomain, TensorProduct
Proof uses: NoZeroDivisors.to_isDomain, NoZeroDivisors.mk, Eq, HMul.hMul, OfNat.ofNat, Exists, Finset, InSubalgebra, Algebra.adjoin, exists_subalgebra_of_tensor, Or, Subalgebra, Union.union, Classical.decEq, LE.le, Algebra.adjoin_mono, Membership.mem, Set, Eq.mpr, id and 27 more
109 instances, coercions and auxiliary constants left out.
Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma alg_closed_alg_ext_equiv_self line 820 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, IsAlgClosed, Algebra, Algebra.IsAlgebraic, Nonempty, AlgEquiv
Proof uses: Nonempty.intro, AlgEquiv.symm, AlgEquiv.ofBijective, Algebra.ofId, And.intro, Function.Injective, AlgHom, Function.Surjective, RingHom.injective, AlgHom.toRingHom, Iff.mp, Eq, WithBot, Nat, Polynomial.degree, minpoly, OfNat.ofNat, Membership.mem, Subring, RingHom.range and 5 more
41 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma isDomain_of_injective line 823 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Function.Injective, IsDomain
Proof uses: IsDomain.mk, NoZeroDivisors.mk, Eq, HMul.hMul, OfNat.ofNat, Eq.mpr, id, congrArg, map_zero, Eq.refl, Or, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero, Eq.mp, map_mul, Or.inl, Eq.trans, Eq.symm, Or.inr, Nontrivial.mk, Exists.intro and 5 more
44 instances, coercions and auxiliary constants left out.
Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma isDomain_tensorProduct_of_isAlgClosed line 844 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsAlgClosed, CommRing, IsDomain, TensorProduct
Proof uses: FractionRing, AlgHom, nonZeroDivisors, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id, Function.Injective, tensorProduct_injective_of_field, IsFractionRing.injective, isDomain_of_injective, AlgHom.toRingHom, isDomain_tensorProduct_of_isAlgClosed_field
74 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ker_Phi_nil line 852 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AlgHom, Membership.mem, Ideal, RingHom.ker, RingHom, AlgHom.toRingHom, IsNilpotent, TensorProduct, Eq, Algebra.TensorProduct.map, AlgHom.id
Proof uses: HasQuotient.Quotient, Ideal.Quotient.mkₐ, Ideal.Quotient.liftₐ, AlgHom.comp, AlgHom.ext, Eq.refl, Function.Injective, Ideal.Quotient.mk, Exists, Ideal.Quotient.mk_surjective, HSub.hSub, OfNat.ofNat, Eq.mpr, id, congrArg, sub_self, map_sub, outParam, MonoidHom, MonoidHom.id and 14 more
129 instances, coercions and auxiliary constants left out.
Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
lemma isPrime_nilradical_of_ker line 895 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Membership.mem, Ideal, RingHom.ker, IsNilpotent, IsDomain, Ideal.IsPrime, nilradical
Proof uses: RingHom.ker_isPrime, Eq, le_antisymm, Submodule, Nat, OfNat.ofNat, HPow.hPow, Eq.mpr, id, congrArg, Iff.mp, Bot.bot, Ideal.mem_bot, map_zero, Eq.refl, Exists.intro, Eq.mp, map_pow, IsNilpotent.eq_zero
53 instances, coercions and auxiliary constants left out.
Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma isPrime_tensorProduct_of_isAlgClosed line 913 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsAlgClosed, CommRing, Ideal.IsPrime, nilradical, TensorProduct
Proof uses: Ideal, HasQuotient.Quotient, FractionRing, AlgHom, Ideal.Quotient.mkₐ, nonZeroDivisors, IsScalarTower.toAlgHom, AlgHom.comp, Algebra.TensorProduct.map, AlgHom.id, RingHom, AlgHom.toRingHom, IsDomain, isDomain_tensorProduct_of_isAlgClosed, Iff.mpr, Ideal.Quotient.isDomain_iff_prime, Membership.mem, RingHom.ker, IsNilpotent, ker_Phi_nil and 14 more
106 instances, coercions and auxiliary constants left out.
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma integralClosure_inv_mem line 941 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Membership.mem, Subalgebra, integralClosure, Inv.inv
Proof uses: IsIntegral.inv
27 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def integralClosure_to_IntermediateField line 944 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IntermediateField
Proof uses: Subalgebra, integralClosure, IntermediateField.mk, Membership.mem, Set, Subsemigroup.carrier, Submonoid.toSubsemigroup, Subsemiring.toSubmonoid, Subalgebra.toSubsemiring, integralClosure_inv_mem
16 instances, coercions and auxiliary constants left out.
lemma isAlgClosed_IntermediateField line 949 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsAlgClosed, Subtype, Membership.mem, IntermediateField, integralClosure_to_IntermediateField
Proof uses: IsAlgClosed.of_exists_root, Polynomial, Polynomial.Monic, Irreducible, Exists.elim, Polynomial.IsRoot, Polynomial.map, algebraMap, Exists, Eq, Polynomial.eval, OfNat.ofNat, IsAlgClosed.exists_root, of_eq_true, Ne, WithBot, Nat, Polynomial.degree, Eq.trans, True and 48 more
83 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma isAlgebraic_IntermediateField line 958 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsAlgebraic, Subtype, Membership.mem, IntermediateField, integralClosure_to_IntermediateField
Proof uses: Algebra.IsAlgebraic.mk, IsIntegral, Subtype.property, Polynomial, And, Polynomial.Monic, Eq, Polynomial.eval₂, algebraMap, OfNat.ofNat, IsAlgebraic, Exists.intro, Ne, AlgHom, Polynomial.aeval, And.intro, Polynomial.Monic.ne_zero, Subtype.ext, of_eq_true, Eq.trans and 18 more
101 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma isPrime_nilradical_of_injective line 973 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Function.Injective, Ideal.IsPrime, nilradical
Proof uses: Ideal.IsPrime.mk, Eq, Ideal, Top.top, Membership.mem, OfNat.ofNat, Eq.mpr, id, congrArg, Submodule.mem_top, Nat, HPow.hPow, False, one_pow, Iff.mp, Bot.bot, Ideal.mem_bot, Eq.mp, Trans.trans, Eq.symm and 17 more
54 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean:340 (same statement text; different proof or body). Qualify references as isPrime_nilradical_of_injective@path.
Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma isPrime_nilradical_equiv line 1015 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, Ideal.IsPrime, nilradical
Proof uses: isPrime_nilradical_of_injective, RingEquiv.toRingHom, RingEquiv.symm, EquivLike.injective
20 instances, coercions and auxiliary constants left out.
def tensor_baseChange_map line 1019 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, TensorProduct, RingHom
Proof uses: AlgHom, Algebra.TensorProduct.includeLeft, AlgHom.comp, AlgHom.restrictScalars, Algebra.TensorProduct.includeRight, Eq, HMul.hMul, AlgHom.toRingHom, Algebra.TensorProduct.lift
80 instances, coercions and auxiliary constants left out.
lemma tensor_baseChange_inj line 1032 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, TensorProduct, Eq, RingHom, algebraMap, TensorProduct.tmul, OfNat.ofNat, Function.Injective, tensor_baseChange_map
Proof uses: AlgHom, Algebra.TensorProduct.includeLeft, AlgHom.comp, AlgHom.restrictScalars, Algebra.TensorProduct.includeRight, HMul.hMul, mul_comm, Algebra.TensorProduct.lift, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, RingHom.toAlgebra, AlgHom.toRingHom, rfl, Eq.mpr, id, congrArg, of_eq_true, eq_self, AlgHom.mk and 13 more
125 instances, coercions and auxiliary constants left out.
Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
lemma irreducibleSpace_baseChange_of_algClosed line 1099 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsAlgClosed, Algebra.IsAlgebraic, IsScalarTower, IrreducibleSpace, PrimeSpectrum, TensorProduct
Proof uses: Ideal.IsPrime, nilradical, Iff.mp, test_nilradical_prime, Algebra.TensorProduct.rightAlgebra, isPrime_tensorProduct_of_isAlgClosed, RingHom, tensor_baseChange_map, Function.Injective, tensor_baseChange_inj, rfl, algebraMap, isPrime_nilradical_of_injective, Iff.mpr
56 instances, coercions and auxiliary constants left out.
Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma irreducibleSpace_baseChange_algClosed line 1114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsAlgClosed, Algebra.IsAlgebraic, IrreducibleSpace, PrimeSpectrum, TensorProduct
Proof uses: IntermediateField, integralClosure_to_IntermediateField, Subtype, Membership.mem, isAlgClosed_IntermediateField, isAlgebraic_IntermediateField, irreducibleSpace_baseChange_of_algClosed
56 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma tfae_3_to_1 line 1124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsSepClosure, IrreducibleSpace, PrimeSpectrum, TensorProduct, GeometricallyIrreducibleAlgebra
Proof uses: IsAlgClosed, Algebra.IsAlgebraic, IntermediateField, separableClosure, Subtype, Membership.mem, test_is_sep_closure, Ideal.IsPrime, nilradical, Iff.mp, test_nilradical_prime, RingHom, AlgHom.toRingHom, Algebra.TensorProduct.map, AlgHom.id, IsScalarTower.toAlgHom, Function.Injective, injective_tensor_extension, Exists, Nat and 15 more
86 instances, coercions and auxiliary constants left out.
Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma isPrime_nilradical_localization line 1146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Submonoid, Ideal.IsPrime, nilradical, Disjoint, Set, Ideal, Localization
Proof uses: Iff.mp, And, and_self_iff, Iff.mpr, Eq.rec, Ideal.map, RingHom, algebraMap, Eq, IsLocalization.isPrime_of_isPrime_disjoint, Eq.symm, le_antisymm, Exists.elim, Prod, Subtype, Membership.mem, IsLocalization.mk'_surjective.match_1, IsLocalization.mk', Submodule, IsLocalization.mk'_surjective and 62 more
109 instances, coercions and auxiliary constants left out.
Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma isPrime_nilradical_polynomial line 1157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal.IsPrime, nilradical, Polynomial
Proof uses: Ideal, RingHom, HasQuotient.Quotient, Polynomial.mapRingHom, Ideal.Quotient.mk, RingHom.ker, RingHom.ker_isPrime, Eq, Ideal.ext, Iff.intro, Membership.mem, OfNat.ofNat, Nat, IsNilpotent, Polynomial.coeff, Eq.mpr, id, congrArg, Polynomial.coeff_zero, Eq.refl and 7 more
47 instances, coercions and auxiliary constants left out.
Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
theorem geometrically_irreducible_tfae line 1196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, List.TFAE, List.cons, GeometricallyIrreducibleAlgebra, Module.Finite, Algebra.IsSeparable, IrreducibleSpace, PrimeSpectrum, TensorProduct, IsSepClosure, IsAlgClosed, List.nil
Proof uses: GeometricallyIrreducibleAlgebra.out, tfae_2_to_3, GeometricallyIrreducibleAlgebra.mk, irreducible_of_algebraic_closed_extension, tfae_3_to_1, List.tfae_of_cycle, List.IsChain.cons_cons, List.IsChain.singleton
42 instances, coercions and auxiliary constants left out.
Tactic trace: 19 steps
Open to load the checked before-and-after goal states.